leoptrt - Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem leoptrt 10072

Description: The positive operator ordering relation is transitive. Exercise 1(iv) of [Retherford] p. 49.

**Assertion**
Ref	Expression
leoptrt	⊢ (((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) ⋀ (S ≤_op T ⋀ T ≤_op U)) → S ≤_op U)

**Proof of Theorem leoptrt**
Step	Hyp	Ref	Expression
1		letrt 5544	. . . . . . 7 ⊢ ((((S ‘x) ·_ih x) ∈ ℝ ⋀ ((T ‘x) ·_ih x) ∈ ℝ ⋀ ((U ‘x) ·_ih x) ∈ ℝ) → ((((S ‘x) ·_ih x) ≤ ((T ‘x) ·_ih x) ⋀ ((T ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)) → ((S ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)))
2		hmopret 9849	. . . . . . 7 ⊢ ((S ∈ HrmOp ⋀ x ∈ ℋ ) → ((S ‘x) ·_ih x) ∈ ℝ)
3		hmopret 9849	. . . . . . 7 ⊢ ((T ∈ HrmOp ⋀ x ∈ ℋ ) → ((T ‘x) ·_ih x) ∈ ℝ)
4		hmopret 9849	. . . . . . 7 ⊢ ((U ∈ HrmOp ⋀ x ∈ ℋ ) → ((U ‘x) ·_ih x) ∈ ℝ)
5	1, 2, 3, 4	syl3an 870	. . . . . 6 ⊢ (((S ∈ HrmOp ⋀ x ∈ ℋ ) ⋀ (T ∈ HrmOp ⋀ x ∈ ℋ ) ⋀ (U ∈ HrmOp ⋀ x ∈ ℋ )) → ((((S ‘x) ·_ih x) ≤ ((T ‘x) ·_ih x) ⋀ ((T ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)) → ((S ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)))
6	5	3anandirs 923	. . . . 5 ⊢ (((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) ⋀ x ∈ ℋ ) → ((((S ‘x) ·_ih x) ≤ ((T ‘x) ·_ih x) ⋀ ((T ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)) → ((S ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)))
7	6	r19.20dva 1712	. . . 4 ⊢ ((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) → (∀x ∈ ℋ (((S ‘x) ·_ih x) ≤ ((T ‘x) ·_ih x) ⋀ ((T ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)) → ∀x ∈ ℋ ((S ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)))
8		r19.26 1753	. . . 4 ⊢ (∀x ∈ ℋ (((S ‘x) ·_ih x) ≤ ((T ‘x) ·_ih x) ⋀ ((T ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)) ↔ (∀x ∈ ℋ ((S ‘x) ·_ih x) ≤ ((T ‘x) ·_ih x) ⋀ ∀x ∈ ℋ ((T ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)))
9	7, 8	syl5ibr 207	. . 3 ⊢ ((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) → ((∀x ∈ ℋ ((S ‘x) ·_ih x) ≤ ((T ‘x) ·_ih x) ⋀ ∀x ∈ ℋ ((T ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)) → ∀x ∈ ℋ ((S ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)))
10		leop2t 10059	. . . . 5 ⊢ ((S ∈ HrmOp ⋀ T ∈ HrmOp) → (S ≤_op T ↔ ∀x ∈ ℋ ((S ‘x) ·_ih x) ≤ ((T ‘x) ·_ih x)))
11	10	3adant3 801	. . . 4 ⊢ ((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) → (S ≤_op T ↔ ∀x ∈ ℋ ((S ‘x) ·_ih x) ≤ ((T ‘x) ·_ih x)))
12		leop2t 10059	. . . . 5 ⊢ ((T ∈ HrmOp ⋀ U ∈ HrmOp) → (T ≤_op U ↔ ∀x ∈ ℋ ((T ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)))
13	12	3adant1 799	. . . 4 ⊢ ((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) → (T ≤_op U ↔ ∀x ∈ ℋ ((T ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)))
14	11, 13	anbi12d 630	. . 3 ⊢ ((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) → ((S ≤_op T ⋀ T ≤_op U) ↔ (∀x ∈ ℋ ((S ‘x) ·_ih x) ≤ ((T ‘x) ·_ih x) ⋀ ∀x ∈ ℋ ((T ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x))))
15		leop2t 10059	. . . 4 ⊢ ((S ∈ HrmOp ⋀ U ∈ HrmOp) → (S ≤_op U ↔ ∀x ∈ ℋ ((S ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)))
16	15	3adant2 800	. . 3 ⊢ ((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) → (S ≤_op U ↔ ∀x ∈ ℋ ((S ‘x) ·_ih x) ≤ ((U ‘x) ·_ih x)))
17	9, 14, 16	3imtr4d 545	. 2 ⊢ ((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) → ((S ≤_op T ⋀ T ≤_op U) → S ≤_op U))
18	17	imp 350	1 ⊢ (((S ∈ HrmOp ⋀ T ∈ HrmOp ⋀ U ∈ HrmOp) ⋀ (S ≤_op T ⋀ T ≤_op U)) → S ≤_op U)

Colors of variables: wff set class

Syntax hints: → wi 3 ↔ wb 146 ⋀ wa 223 ⋀ w3a 777 ∈ wcel 960 ∀wral 1648 class class class wbr 2625 ‘cfv 3189 (class class class)co 3970 ℝcr 5252 ≤ cle 5314 ℋ chil 8790 ·_ih csp 8795 HrmOpcho 8821 ≤_op cleo 8829

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-rep 2699 ax-sep 2709 ax-nul 2716 ax-pow 2749 ax-pr 2786 ax-un 2873 ax-reg 4609 ax-inf2 4641 ax-ac 4761 ax-hilex 8871 ax-hfvadd 8872 ax-hvcom 8873 ax-hvass 8874 ax-hv0cl 8875 ax-hvaddid 8876 ax-hfvmul 8877 ax-hvmulid 8878 ax-hvmulass 8879 ax-hvdistr1 8880 ax-hvdistr2 8881 ax-hvmul0 8882 ax-hfi 8948 ax-his1 8951 ax-his2 8952 ax-his3 8953 ax-his4 8954 ax-hcompl 9073

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 778 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-nel 1591 df-ral 1652 df-rex 1653 df-reu 1654 df-rab 1655 df-v 1815 df-sbc 1945 df-csb 2006 df-dif 2053 df-un 2054 df-in 2055 df-ss 2057 df-pss 2059 df-nul 2285 df-if 2367 df-pw 2407 df-sn 2417 df-pr 2418 df-tp 2420 df-op 2421 df-uni 2509 df-int 2539 df-iun 2573 df-iin 2574 df-br 2626 df-opab 2673 df-tr 2687 df-eprel 2839 df-id 2842 df-po 2847 df-so 2857 df-fr 2924 df-we 2941 df-ord 2958 df-on 2959 df-lim 2960 df-suc 2961 df-om 3139 df-xp 3191 df-rel 3192 df-cnv 3193 df-co 3194 df-dm 3195 df-rn 3196 df-res 3197 df-ima 3198 df-fun 3199 df-fn 3200 df-f 3201 df-f1 3202 df-fo 3203 df-f1o 3204 df-fv 3205 df-rdg 3939 df-opr 3972 df-oprab 3973 df-1st 4086 df-2nd 4087 df-1o 4140 df-oadd 4142 df-omul 4143 df-er 4268 df-ec 4270 df-qs 4273 df-map 4331 df-en 4375 df-dom 4376 df-sdom 4377 df-sup 4590 df-r1 4660 df-rank 4661 df-ni 5019 df-pli 5020 df-mi 5021 df-lti 5022 df-plpq 5054 df-mpq 5055 df-enq 5056 df-nq 5057 df-plq 5058 df-mq 5059 df-rq 5060 df-ltq 5061 df-1q 5062 df-np 5105 df-1p 5106 df-plp 5107 df-mp 5108 df-ltp 5109 df-plpr 5183 df-mpr 5184 df-enr 5185 df-nr 5186 df-plr 5187 df-mr 5188 df-ltr 5189 df-0r 5190 df-1r 5191 df-m1r 5192 df-c 5259 df-0 5260 df-1 5261 df-i 5262 df-r 5263 df-plus 5264 df-mul 5265 df-lt 5266 df-sub 5375 df-neg 5377 df-pnf 5506 df-mnf 5507 df-xr 5508 df-ltxr 5509 df-le 5510 df-div 5722 df-n 5934 df-2 5979 df-3 5980 df-4 5981 df-n0 6109 df-z 6145 df-fl 6233 df-q 6264 df-seq1 6316 df-shft 6349 df-ioo 6369 df-uz 6426 df-fz 6476 df-seqz 6541 df-exp 6577 df-sqr 6678 df-re 6759 df-im 6760 df-cj 6761 df-abs 6762 df-clim 6982 df-sum 6987 df-top 7601 df-bases 7603 df-topgen 7604 df-cld 7667 df-ntr 7668 df-cls 7669 df-cn 7758 df-cnp 7759 df-haus 7786 df-met 7797 df-bl 7799 df-opn 7800 df-lm 7926 df-grp 8041 df-gid 8042 df-ginv 8043 df-gdiv 8044 df-abl 8103 df-vc 8168 df-nv 8214 df-va 8217 df-ba 8218 df-sm 8219 df-0v 8220 df-vs 8221 df-nm 8222 df-ims 8223 df-ip 8353 df-ph 8475 df-hnorm 8839 df-hvsub 8842 df-hlim 8843 df-hcau 8844 df-sh 9078 df-ch 9094 df-oc 9126 df-ch0 9127 df-pj 9239 df-hosum 9508 df-homul 9509 df-hodif 9510 df-h0op 9676 df-hmop 9772 df-leop 9780