Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . 7
⊢ (𝑥 ∈
Cℋ → 𝑥 ∈ Cℋ
) |
2 | | simpl 472 |
. . . . . . 7
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → 𝑢 ∈ ℋ) |
3 | | pjhcl 27644 |
. . . . . . 7
⊢ ((𝑥 ∈
Cℋ ∧ 𝑢 ∈ ℋ) →
((projℎ‘𝑥)‘𝑢) ∈ ℋ) |
4 | 1, 2, 3 | syl2anr 494 |
. . . . . 6
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ ((projℎ‘𝑥)‘𝑢) ∈ ℋ) |
5 | | normcl 27366 |
. . . . . 6
⊢
(((projℎ‘𝑥)‘𝑢) ∈ ℋ →
(normℎ‘((projℎ‘𝑥)‘𝑢)) ∈ ℝ) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ (normℎ‘((projℎ‘𝑥)‘𝑢)) ∈ ℝ) |
7 | 6 | resqcld 12897 |
. . . 4
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ∈ ℝ) |
8 | 6 | sqge0d 12898 |
. . . 4
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ 0 ≤
((normℎ‘((projℎ‘𝑥)‘𝑢))↑2)) |
9 | | normge0 27367 |
. . . . . 6
⊢
(((projℎ‘𝑥)‘𝑢) ∈ ℋ → 0 ≤
(normℎ‘((projℎ‘𝑥)‘𝑢))) |
10 | 4, 9 | syl 17 |
. . . . 5
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ 0 ≤
(normℎ‘((projℎ‘𝑥)‘𝑢))) |
11 | | pjnorm 27967 |
. . . . . . 7
⊢ ((𝑥 ∈
Cℋ ∧ 𝑢 ∈ ℋ) →
(normℎ‘((projℎ‘𝑥)‘𝑢)) ≤ (normℎ‘𝑢)) |
12 | 1, 2, 11 | syl2anr 494 |
. . . . . 6
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ (normℎ‘((projℎ‘𝑥)‘𝑢)) ≤ (normℎ‘𝑢)) |
13 | | simplr 788 |
. . . . . 6
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ (normℎ‘𝑢) = 1) |
14 | 12, 13 | breqtrd 4609 |
. . . . 5
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ (normℎ‘((projℎ‘𝑥)‘𝑢)) ≤ 1) |
15 | | 2nn0 11186 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
16 | | exple1 12782 |
. . . . . 6
⊢
((((normℎ‘((projℎ‘𝑥)‘𝑢)) ∈ ℝ ∧ 0 ≤
(normℎ‘((projℎ‘𝑥)‘𝑢)) ∧
(normℎ‘((projℎ‘𝑥)‘𝑢)) ≤ 1) ∧ 2 ∈
ℕ0) →
((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ≤ 1) |
17 | 15, 16 | mpan2 703 |
. . . . 5
⊢
(((normℎ‘((projℎ‘𝑥)‘𝑢)) ∈ ℝ ∧ 0 ≤
(normℎ‘((projℎ‘𝑥)‘𝑢)) ∧
(normℎ‘((projℎ‘𝑥)‘𝑢)) ≤ 1) →
((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ≤ 1) |
18 | 6, 10, 14, 17 | syl3anc 1318 |
. . . 4
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ≤ 1) |
19 | | 0re 9919 |
. . . . 5
⊢ 0 ∈
ℝ |
20 | | 1re 9918 |
. . . . 5
⊢ 1 ∈
ℝ |
21 | 19, 20 | elicc2i 12110 |
. . . 4
⊢
(((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ∈ (0[,]1) ↔
(((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ∈ ℝ ∧ 0 ≤
((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ∧
((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ≤ 1)) |
22 | 7, 8, 18, 21 | syl3anbrc 1239 |
. . 3
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ∈ (0[,]1)) |
23 | | strlem3a.1 |
. . 3
⊢ 𝑆 = (𝑥 ∈ Cℋ
↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2)) |
24 | 22, 23 | fmptd 6292 |
. 2
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → 𝑆: Cℋ
⟶(0[,]1)) |
25 | | helch 27484 |
. . . 4
⊢ ℋ
∈ Cℋ |
26 | 23 | strlem2 28494 |
. . . 4
⊢ ( ℋ
∈ Cℋ → (𝑆‘ ℋ) =
((normℎ‘((projℎ‘
ℋ)‘𝑢))↑2)) |
27 | 25, 26 | ax-mp 5 |
. . 3
⊢ (𝑆‘ ℋ) =
((normℎ‘((projℎ‘
ℋ)‘𝑢))↑2) |
28 | | pjch1 27913 |
. . . . . 6
⊢ (𝑢 ∈ ℋ →
((projℎ‘ ℋ)‘𝑢) = 𝑢) |
29 | 28 | fveq2d 6107 |
. . . . 5
⊢ (𝑢 ∈ ℋ →
(normℎ‘((projℎ‘
ℋ)‘𝑢)) =
(normℎ‘𝑢)) |
30 | 29 | oveq1d 6564 |
. . . 4
⊢ (𝑢 ∈ ℋ →
((normℎ‘((projℎ‘
ℋ)‘𝑢))↑2)
= ((normℎ‘𝑢)↑2)) |
31 | | oveq1 6556 |
. . . . 5
⊢
((normℎ‘𝑢) = 1 →
((normℎ‘𝑢)↑2) = (1↑2)) |
32 | | sq1 12820 |
. . . . 5
⊢
(1↑2) = 1 |
33 | 31, 32 | syl6eq 2660 |
. . . 4
⊢
((normℎ‘𝑢) = 1 →
((normℎ‘𝑢)↑2) = 1) |
34 | 30, 33 | sylan9eq 2664 |
. . 3
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) →
((normℎ‘((projℎ‘
ℋ)‘𝑢))↑2)
= 1) |
35 | 27, 34 | syl5eq 2656 |
. 2
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → (𝑆‘ ℋ) = 1) |
36 | | pjcjt2 27935 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
→ (𝑧 ⊆
(⊥‘𝑤) →
((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢) = (((projℎ‘𝑧)‘𝑢) +ℎ
((projℎ‘𝑤)‘𝑢)))) |
37 | 36 | imp 444 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢) = (((projℎ‘𝑧)‘𝑢) +ℎ
((projℎ‘𝑤)‘𝑢))) |
38 | 37 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
(normℎ‘((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢)) =
(normℎ‘(((projℎ‘𝑧)‘𝑢) +ℎ
((projℎ‘𝑤)‘𝑢)))) |
39 | 38 | oveq1d 6564 |
. . . . . . . . 9
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
((normℎ‘((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢))↑2) =
((normℎ‘(((projℎ‘𝑧)‘𝑢) +ℎ
((projℎ‘𝑤)‘𝑢)))↑2)) |
40 | | pjopyth 27963 |
. . . . . . . . . 10
⊢ ((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
→ (𝑧 ⊆
(⊥‘𝑤) →
((normℎ‘(((projℎ‘𝑧)‘𝑢) +ℎ
((projℎ‘𝑤)‘𝑢)))↑2) =
(((normℎ‘((projℎ‘𝑧)‘𝑢))↑2) +
((normℎ‘((projℎ‘𝑤)‘𝑢))↑2)))) |
41 | 40 | imp 444 |
. . . . . . . . 9
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
((normℎ‘(((projℎ‘𝑧)‘𝑢) +ℎ
((projℎ‘𝑤)‘𝑢)))↑2) =
(((normℎ‘((projℎ‘𝑧)‘𝑢))↑2) +
((normℎ‘((projℎ‘𝑤)‘𝑢))↑2))) |
42 | 39, 41 | eqtrd 2644 |
. . . . . . . 8
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
((normℎ‘((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢))↑2) =
(((normℎ‘((projℎ‘𝑧)‘𝑢))↑2) +
((normℎ‘((projℎ‘𝑤)‘𝑢))↑2))) |
43 | | chjcl 27600 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ )
→ (𝑧
∨ℋ 𝑤)
∈ Cℋ ) |
44 | 43 | 3adant3 1074 |
. . . . . . . . . 10
⊢ ((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
→ (𝑧
∨ℋ 𝑤)
∈ Cℋ ) |
45 | 44 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
(𝑧 ∨ℋ
𝑤) ∈
Cℋ ) |
46 | 23 | strlem2 28494 |
. . . . . . . . 9
⊢ ((𝑧 ∨ℋ 𝑤) ∈
Cℋ → (𝑆‘(𝑧 ∨ℋ 𝑤)) =
((normℎ‘((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢))↑2)) |
47 | 45, 46 | syl 17 |
. . . . . . . 8
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
(𝑆‘(𝑧 ∨ℋ 𝑤)) =
((normℎ‘((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢))↑2)) |
48 | | 3simpa 1051 |
. . . . . . . . . 10
⊢ ((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
→ (𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
)) |
49 | 48 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
(𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
)) |
50 | 23 | strlem2 28494 |
. . . . . . . . . 10
⊢ (𝑧 ∈
Cℋ → (𝑆‘𝑧) =
((normℎ‘((projℎ‘𝑧)‘𝑢))↑2)) |
51 | 23 | strlem2 28494 |
. . . . . . . . . 10
⊢ (𝑤 ∈
Cℋ → (𝑆‘𝑤) =
((normℎ‘((projℎ‘𝑤)‘𝑢))↑2)) |
52 | 50, 51 | oveqan12d 6568 |
. . . . . . . . 9
⊢ ((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ )
→ ((𝑆‘𝑧) + (𝑆‘𝑤)) =
(((normℎ‘((projℎ‘𝑧)‘𝑢))↑2) +
((normℎ‘((projℎ‘𝑤)‘𝑢))↑2))) |
53 | 49, 52 | syl 17 |
. . . . . . . 8
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
((𝑆‘𝑧) + (𝑆‘𝑤)) =
(((normℎ‘((projℎ‘𝑧)‘𝑢))↑2) +
((normℎ‘((projℎ‘𝑤)‘𝑢))↑2))) |
54 | 42, 47, 53 | 3eqtr4d 2654 |
. . . . . . 7
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
(𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤))) |
55 | 54 | 3exp1 1275 |
. . . . . 6
⊢ (𝑧 ∈
Cℋ → (𝑤 ∈ Cℋ
→ (𝑢 ∈ ℋ
→ (𝑧 ⊆
(⊥‘𝑤) →
(𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤)))))) |
56 | 55 | com3r 85 |
. . . . 5
⊢ (𝑢 ∈ ℋ → (𝑧 ∈
Cℋ → (𝑤 ∈ Cℋ
→ (𝑧 ⊆
(⊥‘𝑤) →
(𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤)))))) |
57 | 56 | adantr 480 |
. . . 4
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → (𝑧 ∈ Cℋ
→ (𝑤 ∈
Cℋ → (𝑧 ⊆ (⊥‘𝑤) → (𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤)))))) |
58 | 57 | ralrimdv 2951 |
. . 3
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → (𝑧 ∈ Cℋ
→ ∀𝑤 ∈
Cℋ (𝑧 ⊆ (⊥‘𝑤) → (𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤))))) |
59 | 58 | ralrimiv 2948 |
. 2
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → ∀𝑧 ∈ Cℋ
∀𝑤 ∈
Cℋ (𝑧 ⊆ (⊥‘𝑤) → (𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤)))) |
60 | | isst 28456 |
. 2
⊢ (𝑆 ∈ States ↔ (𝑆:
Cℋ ⟶(0[,]1) ∧ (𝑆‘ ℋ) = 1 ∧ ∀𝑧 ∈
Cℋ ∀𝑤 ∈ Cℋ
(𝑧 ⊆
(⊥‘𝑤) →
(𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤))))) |
61 | 24, 35, 59, 60 | syl3anbrc 1239 |
1
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → 𝑆 ∈ States) |