Proof of Theorem hstle
Step | Hyp | Ref
| Expression |
1 | | hstnmoc 30304 |
. . . . . . . 8
⊢ ((𝑆 ∈ CHStates ∧ 𝐵 ∈
Cℋ ) →
(((normℎ‘(𝑆‘𝐵))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)) = 1) |
2 | 1 | adantlr 715 |
. . . . . . 7
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ (((normℎ‘(𝑆‘𝐵))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)) = 1) |
3 | 2 | oveq2d 7229 |
. . . . . 6
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ (((normℎ‘(𝑆‘𝐴))↑2) +
(((normℎ‘(𝑆‘𝐵))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2))) =
(((normℎ‘(𝑆‘𝐴))↑2) + 1)) |
4 | | hstcl 30298 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) → (𝑆‘𝐴) ∈ ℋ) |
5 | | normcl 29206 |
. . . . . . . . . . 11
⊢ ((𝑆‘𝐴) ∈ ℋ →
(normℎ‘(𝑆‘𝐴)) ∈ ℝ) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) →
(normℎ‘(𝑆‘𝐴)) ∈ ℝ) |
7 | 6 | resqcld 13817 |
. . . . . . . . 9
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) →
((normℎ‘(𝑆‘𝐴))↑2) ∈ ℝ) |
8 | 7 | adantr 484 |
. . . . . . . 8
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ ((normℎ‘(𝑆‘𝐴))↑2) ∈ ℝ) |
9 | 8 | recnd 10861 |
. . . . . . 7
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ ((normℎ‘(𝑆‘𝐴))↑2) ∈ ℂ) |
10 | | hstcl 30298 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ CHStates ∧ 𝐵 ∈
Cℋ ) → (𝑆‘𝐵) ∈ ℋ) |
11 | | normcl 29206 |
. . . . . . . . . . 11
⊢ ((𝑆‘𝐵) ∈ ℋ →
(normℎ‘(𝑆‘𝐵)) ∈ ℝ) |
12 | 10, 11 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ CHStates ∧ 𝐵 ∈
Cℋ ) →
(normℎ‘(𝑆‘𝐵)) ∈ ℝ) |
13 | 12 | resqcld 13817 |
. . . . . . . . 9
⊢ ((𝑆 ∈ CHStates ∧ 𝐵 ∈
Cℋ ) →
((normℎ‘(𝑆‘𝐵))↑2) ∈ ℝ) |
14 | 13 | adantlr 715 |
. . . . . . . 8
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ ((normℎ‘(𝑆‘𝐵))↑2) ∈ ℝ) |
15 | 14 | recnd 10861 |
. . . . . . 7
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ ((normℎ‘(𝑆‘𝐵))↑2) ∈ ℂ) |
16 | | choccl 29387 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈
Cℋ → (⊥‘𝐵) ∈ Cℋ
) |
17 | | hstcl 30298 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ CHStates ∧
(⊥‘𝐵) ∈
Cℋ ) → (𝑆‘(⊥‘𝐵)) ∈ ℋ) |
18 | 16, 17 | sylan2 596 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ CHStates ∧ 𝐵 ∈
Cℋ ) → (𝑆‘(⊥‘𝐵)) ∈ ℋ) |
19 | | normcl 29206 |
. . . . . . . . . . 11
⊢ ((𝑆‘(⊥‘𝐵)) ∈ ℋ →
(normℎ‘(𝑆‘(⊥‘𝐵))) ∈ ℝ) |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ CHStates ∧ 𝐵 ∈
Cℋ ) →
(normℎ‘(𝑆‘(⊥‘𝐵))) ∈ ℝ) |
21 | 20 | resqcld 13817 |
. . . . . . . . 9
⊢ ((𝑆 ∈ CHStates ∧ 𝐵 ∈
Cℋ ) →
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2) ∈ ℝ) |
22 | 21 | adantlr 715 |
. . . . . . . 8
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ ((normℎ‘(𝑆‘(⊥‘𝐵)))↑2) ∈ ℝ) |
23 | 22 | recnd 10861 |
. . . . . . 7
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ ((normℎ‘(𝑆‘(⊥‘𝐵)))↑2) ∈ ℂ) |
24 | 9, 15, 23 | add12d 11058 |
. . . . . 6
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ (((normℎ‘(𝑆‘𝐴))↑2) +
(((normℎ‘(𝑆‘𝐵))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2))) =
(((normℎ‘(𝑆‘𝐵))↑2) +
(((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)))) |
25 | 3, 24 | eqtr3d 2779 |
. . . . 5
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ (((normℎ‘(𝑆‘𝐴))↑2) + 1) =
(((normℎ‘(𝑆‘𝐵))↑2) +
(((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)))) |
26 | 25 | adantrr 717 |
. . . 4
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆ 𝐵)) →
(((normℎ‘(𝑆‘𝐴))↑2) + 1) =
(((normℎ‘(𝑆‘𝐵))↑2) +
(((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)))) |
27 | 16 | adantr 484 |
. . . . . . . 8
⊢ ((𝐵 ∈
Cℋ ∧ 𝐴 ⊆ 𝐵) → (⊥‘𝐵) ∈ Cℋ
) |
28 | | ococ 29487 |
. . . . . . . . . 10
⊢ (𝐵 ∈
Cℋ → (⊥‘(⊥‘𝐵)) = 𝐵) |
29 | 28 | sseq2d 3933 |
. . . . . . . . 9
⊢ (𝐵 ∈
Cℋ → (𝐴 ⊆ (⊥‘(⊥‘𝐵)) ↔ 𝐴 ⊆ 𝐵)) |
30 | 29 | biimpar 481 |
. . . . . . . 8
⊢ ((𝐵 ∈
Cℋ ∧ 𝐴 ⊆ 𝐵) → 𝐴 ⊆ (⊥‘(⊥‘𝐵))) |
31 | 27, 30 | jca 515 |
. . . . . . 7
⊢ ((𝐵 ∈
Cℋ ∧ 𝐴 ⊆ 𝐵) → ((⊥‘𝐵) ∈ Cℋ
∧ 𝐴 ⊆
(⊥‘(⊥‘𝐵)))) |
32 | | hstpyth 30310 |
. . . . . . 7
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ ((⊥‘𝐵) ∈ Cℋ
∧ 𝐴 ⊆
(⊥‘(⊥‘𝐵)))) →
((normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))))↑2) =
(((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2))) |
33 | 31, 32 | sylan2 596 |
. . . . . 6
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆ 𝐵)) →
((normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))))↑2) =
(((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2))) |
34 | | chjcl 29438 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈
Cℋ ∧ (⊥‘𝐵) ∈ Cℋ )
→ (𝐴
∨ℋ (⊥‘𝐵)) ∈ Cℋ
) |
35 | 16, 34 | sylan2 596 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ )
→ (𝐴
∨ℋ (⊥‘𝐵)) ∈ Cℋ
) |
36 | | hstcl 30298 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ CHStates ∧ (𝐴 ∨ℋ
(⊥‘𝐵)) ∈
Cℋ ) → (𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))) ∈
ℋ) |
37 | 35, 36 | sylan2 596 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ CHStates ∧ (𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ ))
→ (𝑆‘(𝐴 ∨ℋ
(⊥‘𝐵))) ∈
ℋ) |
38 | 37 | anassrs 471 |
. . . . . . . . . 10
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ (𝑆‘(𝐴 ∨ℋ
(⊥‘𝐵))) ∈
ℋ) |
39 | | normcl 29206 |
. . . . . . . . . 10
⊢ ((𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))) ∈ ℋ →
(normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵)))) ∈
ℝ) |
40 | 38, 39 | syl 17 |
. . . . . . . . 9
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ (normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵)))) ∈
ℝ) |
41 | | normge0 29207 |
. . . . . . . . . 10
⊢ ((𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))) ∈ ℋ → 0 ≤
(normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))))) |
42 | 38, 41 | syl 17 |
. . . . . . . . 9
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ 0 ≤ (normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))))) |
43 | | hstle1 30307 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ CHStates ∧ (𝐴 ∨ℋ
(⊥‘𝐵)) ∈
Cℋ ) →
(normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵)))) ≤ 1) |
44 | 35, 43 | sylan2 596 |
. . . . . . . . . 10
⊢ ((𝑆 ∈ CHStates ∧ (𝐴 ∈
Cℋ ∧ 𝐵 ∈ Cℋ ))
→ (normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵)))) ≤ 1) |
45 | 44 | anassrs 471 |
. . . . . . . . 9
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ (normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵)))) ≤ 1) |
46 | | 1re 10833 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
47 | | le2sq2 13706 |
. . . . . . . . . 10
⊢
((((normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵)))) ∈ ℝ ∧ 0 ≤
(normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))))) ∧ (1 ∈ ℝ
∧ (normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵)))) ≤ 1)) →
((normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))))↑2) ≤
(1↑2)) |
48 | 46, 47 | mpanr1 703 |
. . . . . . . . 9
⊢
((((normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵)))) ∈ ℝ ∧ 0 ≤
(normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))))) ∧
(normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵)))) ≤ 1) →
((normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))))↑2) ≤
(1↑2)) |
49 | 40, 42, 45, 48 | syl21anc 838 |
. . . . . . . 8
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ ((normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))))↑2) ≤
(1↑2)) |
50 | | sq1 13764 |
. . . . . . . 8
⊢
(1↑2) = 1 |
51 | 49, 50 | breqtrdi 5094 |
. . . . . . 7
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ ((normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))))↑2) ≤
1) |
52 | 51 | adantrr 717 |
. . . . . 6
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆ 𝐵)) →
((normℎ‘(𝑆‘(𝐴 ∨ℋ (⊥‘𝐵))))↑2) ≤
1) |
53 | 33, 52 | eqbrtrrd 5077 |
. . . . 5
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆ 𝐵)) →
(((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)) ≤ 1) |
54 | 8, 22 | readdcld 10862 |
. . . . . . 7
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ (((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)) ∈
ℝ) |
55 | | leadd2 11301 |
. . . . . . . 8
⊢
(((((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)) ∈ ℝ ∧ 1 ∈
ℝ ∧ ((normℎ‘(𝑆‘𝐵))↑2) ∈ ℝ) →
((((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)) ≤ 1 ↔
(((normℎ‘(𝑆‘𝐵))↑2) +
(((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2))) ≤
(((normℎ‘(𝑆‘𝐵))↑2) + 1))) |
56 | 46, 55 | mp3an2 1451 |
. . . . . . 7
⊢
(((((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)) ∈ ℝ ∧
((normℎ‘(𝑆‘𝐵))↑2) ∈ ℝ) →
((((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)) ≤ 1 ↔
(((normℎ‘(𝑆‘𝐵))↑2) +
(((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2))) ≤
(((normℎ‘(𝑆‘𝐵))↑2) + 1))) |
57 | 54, 14, 56 | syl2anc 587 |
. . . . . 6
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ ((((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)) ≤ 1 ↔
(((normℎ‘(𝑆‘𝐵))↑2) +
(((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2))) ≤
(((normℎ‘(𝑆‘𝐵))↑2) + 1))) |
58 | 57 | adantrr 717 |
. . . . 5
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆ 𝐵)) →
((((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2)) ≤ 1 ↔
(((normℎ‘(𝑆‘𝐵))↑2) +
(((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2))) ≤
(((normℎ‘(𝑆‘𝐵))↑2) + 1))) |
59 | 53, 58 | mpbid 235 |
. . . 4
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆ 𝐵)) →
(((normℎ‘(𝑆‘𝐵))↑2) +
(((normℎ‘(𝑆‘𝐴))↑2) +
((normℎ‘(𝑆‘(⊥‘𝐵)))↑2))) ≤
(((normℎ‘(𝑆‘𝐵))↑2) + 1)) |
60 | 26, 59 | eqbrtrd 5075 |
. . 3
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆ 𝐵)) →
(((normℎ‘(𝑆‘𝐴))↑2) + 1) ≤
(((normℎ‘(𝑆‘𝐵))↑2) + 1)) |
61 | | leadd1 11300 |
. . . . . 6
⊢
((((normℎ‘(𝑆‘𝐴))↑2) ∈ ℝ ∧
((normℎ‘(𝑆‘𝐵))↑2) ∈ ℝ ∧ 1 ∈
ℝ) → (((normℎ‘(𝑆‘𝐴))↑2) ≤
((normℎ‘(𝑆‘𝐵))↑2) ↔
(((normℎ‘(𝑆‘𝐴))↑2) + 1) ≤
(((normℎ‘(𝑆‘𝐵))↑2) + 1))) |
62 | 46, 61 | mp3an3 1452 |
. . . . 5
⊢
((((normℎ‘(𝑆‘𝐴))↑2) ∈ ℝ ∧
((normℎ‘(𝑆‘𝐵))↑2) ∈ ℝ) →
(((normℎ‘(𝑆‘𝐴))↑2) ≤
((normℎ‘(𝑆‘𝐵))↑2) ↔
(((normℎ‘(𝑆‘𝐴))↑2) + 1) ≤
(((normℎ‘(𝑆‘𝐵))↑2) + 1))) |
63 | 8, 14, 62 | syl2anc 587 |
. . . 4
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ (((normℎ‘(𝑆‘𝐴))↑2) ≤
((normℎ‘(𝑆‘𝐵))↑2) ↔
(((normℎ‘(𝑆‘𝐴))↑2) + 1) ≤
(((normℎ‘(𝑆‘𝐵))↑2) + 1))) |
64 | 63 | adantrr 717 |
. . 3
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆ 𝐵)) →
(((normℎ‘(𝑆‘𝐴))↑2) ≤
((normℎ‘(𝑆‘𝐵))↑2) ↔
(((normℎ‘(𝑆‘𝐴))↑2) + 1) ≤
(((normℎ‘(𝑆‘𝐵))↑2) + 1))) |
65 | 60, 64 | mpbird 260 |
. 2
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆ 𝐵)) →
((normℎ‘(𝑆‘𝐴))↑2) ≤
((normℎ‘(𝑆‘𝐵))↑2)) |
66 | | normge0 29207 |
. . . . . . 7
⊢ ((𝑆‘𝐴) ∈ ℋ → 0 ≤
(normℎ‘(𝑆‘𝐴))) |
67 | 4, 66 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) → 0 ≤
(normℎ‘(𝑆‘𝐴))) |
68 | 6, 67 | jca 515 |
. . . . 5
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) →
((normℎ‘(𝑆‘𝐴)) ∈ ℝ ∧ 0 ≤
(normℎ‘(𝑆‘𝐴)))) |
69 | 68 | adantr 484 |
. . . 4
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ ((normℎ‘(𝑆‘𝐴)) ∈ ℝ ∧ 0 ≤
(normℎ‘(𝑆‘𝐴)))) |
70 | | normge0 29207 |
. . . . . . 7
⊢ ((𝑆‘𝐵) ∈ ℋ → 0 ≤
(normℎ‘(𝑆‘𝐵))) |
71 | 10, 70 | syl 17 |
. . . . . 6
⊢ ((𝑆 ∈ CHStates ∧ 𝐵 ∈
Cℋ ) → 0 ≤
(normℎ‘(𝑆‘𝐵))) |
72 | 12, 71 | jca 515 |
. . . . 5
⊢ ((𝑆 ∈ CHStates ∧ 𝐵 ∈
Cℋ ) →
((normℎ‘(𝑆‘𝐵)) ∈ ℝ ∧ 0 ≤
(normℎ‘(𝑆‘𝐵)))) |
73 | 72 | adantlr 715 |
. . . 4
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ ((normℎ‘(𝑆‘𝐵)) ∈ ℝ ∧ 0 ≤
(normℎ‘(𝑆‘𝐵)))) |
74 | | le2sq 13705 |
. . . 4
⊢
((((normℎ‘(𝑆‘𝐴)) ∈ ℝ ∧ 0 ≤
(normℎ‘(𝑆‘𝐴))) ∧
((normℎ‘(𝑆‘𝐵)) ∈ ℝ ∧ 0 ≤
(normℎ‘(𝑆‘𝐵)))) →
((normℎ‘(𝑆‘𝐴)) ≤
(normℎ‘(𝑆‘𝐵)) ↔
((normℎ‘(𝑆‘𝐴))↑2) ≤
((normℎ‘(𝑆‘𝐵))↑2))) |
75 | 69, 73, 74 | syl2anc 587 |
. . 3
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ 𝐵 ∈ Cℋ )
→ ((normℎ‘(𝑆‘𝐴)) ≤
(normℎ‘(𝑆‘𝐵)) ↔
((normℎ‘(𝑆‘𝐴))↑2) ≤
((normℎ‘(𝑆‘𝐵))↑2))) |
76 | 75 | adantrr 717 |
. 2
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆ 𝐵)) →
((normℎ‘(𝑆‘𝐴)) ≤
(normℎ‘(𝑆‘𝐵)) ↔
((normℎ‘(𝑆‘𝐴))↑2) ≤
((normℎ‘(𝑆‘𝐵))↑2))) |
77 | 65, 76 | mpbird 260 |
1
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈
Cℋ ) ∧ (𝐵 ∈ Cℋ
∧ 𝐴 ⊆ 𝐵)) →
(normℎ‘(𝑆‘𝐴)) ≤
(normℎ‘(𝑆‘𝐵))) |