Metamath Proof Explorer

Theorem hstle

Description: Ordering property of a Hilbert-space-valued state. (Contributed by NM, 26-Jun-2006) (New usage is discouraged.)

Ref Expression
Assertion hstle ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ∧A⊆B→normℎ⁡S⁡A≤normℎ⁡S⁡B

Proof

Step Hyp Ref Expression
1 hstnmoc ⊢S∈CHStates∧B∈Cℋ→normℎ⁡S⁡B2+normℎ⁡S⁡⊥⁡B2=1
2 1 adantlr ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡B2+normℎ⁡S⁡⊥⁡B2=1
3 2 oveq2d ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A2+normℎ⁡S⁡B2+normℎ⁡S⁡⊥⁡B2=normℎ⁡S⁡A2+1
4 hstcl ⊢S∈CHStates∧A∈Cℋ→S⁡A∈ℋ
5 normcl ⊢S⁡A∈ℋ→normℎ⁡S⁡A∈ℝ
6 4 5 syl ⊢S∈CHStates∧A∈Cℋ→normℎ⁡S⁡A∈ℝ
7 6 resqcld ⊢S∈CHStates∧A∈Cℋ→normℎ⁡S⁡A2∈ℝ
8 7 adantr ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A2∈ℝ
9 8 recnd ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A2∈ℂ
10 hstcl ⊢S∈CHStates∧B∈Cℋ→S⁡B∈ℋ
11 normcl ⊢S⁡B∈ℋ→normℎ⁡S⁡B∈ℝ
12 10 11 syl ⊢S∈CHStates∧B∈Cℋ→normℎ⁡S⁡B∈ℝ
13 12 resqcld ⊢S∈CHStates∧B∈Cℋ→normℎ⁡S⁡B2∈ℝ
14 13 adantlr ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡B2∈ℝ
15 14 recnd ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡B2∈ℂ
16 choccl ⊢B∈Cℋ→⊥⁡B∈Cℋ
17 hstcl ⊢S∈CHStates∧⊥⁡B∈Cℋ→S⁡⊥⁡B∈ℋ
18 16 17 sylan2 ⊢S∈CHStates∧B∈Cℋ→S⁡⊥⁡B∈ℋ
19 normcl ⊢S⁡⊥⁡B∈ℋ→normℎ⁡S⁡⊥⁡B∈ℝ
20 18 19 syl ⊢S∈CHStates∧B∈Cℋ→normℎ⁡S⁡⊥⁡B∈ℝ
21 20 resqcld ⊢S∈CHStates∧B∈Cℋ→normℎ⁡S⁡⊥⁡B2∈ℝ
22 21 adantlr ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡⊥⁡B2∈ℝ
23 22 recnd ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡⊥⁡B2∈ℂ
24 9 15 23 add12d ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A2+normℎ⁡S⁡B2+normℎ⁡S⁡⊥⁡B2=normℎ⁡S⁡B2+normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2
25 3 24 eqtr3d ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A2+1=normℎ⁡S⁡B2+normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2
26 25 adantrr ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ∧A⊆B→normℎ⁡S⁡A2+1=normℎ⁡S⁡B2+normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2
27 16 adantr ⊢B∈Cℋ∧A⊆B→⊥⁡B∈Cℋ
28 ococ ⊢B∈Cℋ→⊥⁡⊥⁡B=B
29 28 sseq2d ⊢B∈Cℋ→A⊆⊥⁡⊥⁡B↔A⊆B
30 29 biimpar ⊢B∈Cℋ∧A⊆B→A⊆⊥⁡⊥⁡B
31 27 30 jca ⊢B∈Cℋ∧A⊆B→⊥⁡B∈Cℋ∧A⊆⊥⁡⊥⁡B
32 hstpyth ⊢S∈CHStates∧A∈Cℋ∧⊥⁡B∈Cℋ∧A⊆⊥⁡⊥⁡B→normℎ⁡S⁡A∨ℋ⊥⁡B2=normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2
33 31 32 sylan2 ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ∧A⊆B→normℎ⁡S⁡A∨ℋ⊥⁡B2=normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2
34 chjcl ⊢A∈Cℋ∧⊥⁡B∈Cℋ→A∨ℋ⊥⁡B∈Cℋ
35 16 34 sylan2 ⊢A∈Cℋ∧B∈Cℋ→A∨ℋ⊥⁡B∈Cℋ
36 hstcl ⊢S∈CHStates∧A∨ℋ⊥⁡B∈Cℋ→S⁡A∨ℋ⊥⁡B∈ℋ
37 35 36 sylan2 ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→S⁡A∨ℋ⊥⁡B∈ℋ
38 37 anassrs ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→S⁡A∨ℋ⊥⁡B∈ℋ
39 normcl ⊢S⁡A∨ℋ⊥⁡B∈ℋ→normℎ⁡S⁡A∨ℋ⊥⁡B∈ℝ
40 38 39 syl ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A∨ℋ⊥⁡B∈ℝ
41 normge0 ⊢S⁡A∨ℋ⊥⁡B∈ℋ→0≤normℎ⁡S⁡A∨ℋ⊥⁡B
42 38 41 syl ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→0≤normℎ⁡S⁡A∨ℋ⊥⁡B
43 hstle1 ⊢S∈CHStates∧A∨ℋ⊥⁡B∈Cℋ→normℎ⁡S⁡A∨ℋ⊥⁡B≤1
44 35 43 sylan2 ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A∨ℋ⊥⁡B≤1
45 44 anassrs ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A∨ℋ⊥⁡B≤1
46 1re ⊢1∈ℝ
47 le2sq2 ⊢normℎ⁡S⁡A∨ℋ⊥⁡B∈ℝ∧0≤normℎ⁡S⁡A∨ℋ⊥⁡B∧1∈ℝ∧normℎ⁡S⁡A∨ℋ⊥⁡B≤1→normℎ⁡S⁡A∨ℋ⊥⁡B2≤12
48 46 47 mpanr1 ⊢normℎ⁡S⁡A∨ℋ⊥⁡B∈ℝ∧0≤normℎ⁡S⁡A∨ℋ⊥⁡B∧normℎ⁡S⁡A∨ℋ⊥⁡B≤1→normℎ⁡S⁡A∨ℋ⊥⁡B2≤12
49 40 42 45 48 syl21anc ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A∨ℋ⊥⁡B2≤12
50 sq1 ⊢12=1
51 49 50 breqtrdi ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A∨ℋ⊥⁡B2≤1
52 51 adantrr ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ∧A⊆B→normℎ⁡S⁡A∨ℋ⊥⁡B2≤1
53 33 52 eqbrtrrd ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ∧A⊆B→normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2≤1
54 8 22 readdcld ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2∈ℝ
55 leadd2 ⊢normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2∈ℝ∧1∈ℝ∧normℎ⁡S⁡B2∈ℝ→normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2≤1↔normℎ⁡S⁡B2+normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2≤normℎ⁡S⁡B2+1
56 46 55 mp3an2 ⊢normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2∈ℝ∧normℎ⁡S⁡B2∈ℝ→normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2≤1↔normℎ⁡S⁡B2+normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2≤normℎ⁡S⁡B2+1
57 54 14 56 syl2anc ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2≤1↔normℎ⁡S⁡B2+normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2≤normℎ⁡S⁡B2+1
58 57 adantrr ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ∧A⊆B→normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2≤1↔normℎ⁡S⁡B2+normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2≤normℎ⁡S⁡B2+1
59 53 58 mpbid ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ∧A⊆B→normℎ⁡S⁡B2+normℎ⁡S⁡A2+normℎ⁡S⁡⊥⁡B2≤normℎ⁡S⁡B2+1
60 26 59 eqbrtrd ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ∧A⊆B→normℎ⁡S⁡A2+1≤normℎ⁡S⁡B2+1
61 leadd1 ⊢normℎ⁡S⁡A2∈ℝ∧normℎ⁡S⁡B2∈ℝ∧1∈ℝ→normℎ⁡S⁡A2≤normℎ⁡S⁡B2↔normℎ⁡S⁡A2+1≤normℎ⁡S⁡B2+1
62 46 61 mp3an3 ⊢normℎ⁡S⁡A2∈ℝ∧normℎ⁡S⁡B2∈ℝ→normℎ⁡S⁡A2≤normℎ⁡S⁡B2↔normℎ⁡S⁡A2+1≤normℎ⁡S⁡B2+1
63 8 14 62 syl2anc ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A2≤normℎ⁡S⁡B2↔normℎ⁡S⁡A2+1≤normℎ⁡S⁡B2+1
64 63 adantrr ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ∧A⊆B→normℎ⁡S⁡A2≤normℎ⁡S⁡B2↔normℎ⁡S⁡A2+1≤normℎ⁡S⁡B2+1
65 60 64 mpbird ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ∧A⊆B→normℎ⁡S⁡A2≤normℎ⁡S⁡B2
66 normge0 ⊢S⁡A∈ℋ→0≤normℎ⁡S⁡A
67 4 66 syl ⊢S∈CHStates∧A∈Cℋ→0≤normℎ⁡S⁡A
68 6 67 jca ⊢S∈CHStates∧A∈Cℋ→normℎ⁡S⁡A∈ℝ∧0≤normℎ⁡S⁡A
69 68 adantr ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A∈ℝ∧0≤normℎ⁡S⁡A
70 normge0 ⊢S⁡B∈ℋ→0≤normℎ⁡S⁡B
71 10 70 syl ⊢S∈CHStates∧B∈Cℋ→0≤normℎ⁡S⁡B
72 12 71 jca ⊢S∈CHStates∧B∈Cℋ→normℎ⁡S⁡B∈ℝ∧0≤normℎ⁡S⁡B
73 72 adantlr ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡B∈ℝ∧0≤normℎ⁡S⁡B
74 le2sq ⊢normℎ⁡S⁡A∈ℝ∧0≤normℎ⁡S⁡A∧normℎ⁡S⁡B∈ℝ∧0≤normℎ⁡S⁡B→normℎ⁡S⁡A≤normℎ⁡S⁡B↔normℎ⁡S⁡A2≤normℎ⁡S⁡B2
75 69 73 74 syl2anc ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ→normℎ⁡S⁡A≤normℎ⁡S⁡B↔normℎ⁡S⁡A2≤normℎ⁡S⁡B2
76 75 adantrr ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ∧A⊆B→normℎ⁡S⁡A≤normℎ⁡S⁡B↔normℎ⁡S⁡A2≤normℎ⁡S⁡B2
77 65 76 mpbird ⊢S∈CHStates∧A∈Cℋ∧B∈Cℋ∧A⊆B→normℎ⁡S⁡A≤normℎ⁡S⁡B