Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . . . . 7
⊢ (𝑥 ∈
Cℋ → 𝑥 ∈ Cℋ
) |
2 | | simpl 483 |
. . . . . . 7
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → 𝑢 ∈ ℋ) |
3 | | pjhcl 29763 |
. . . . . . 7
⊢ ((𝑥 ∈
Cℋ ∧ 𝑢 ∈ ℋ) →
((projℎ‘𝑥)‘𝑢) ∈ ℋ) |
4 | 1, 2, 3 | syl2anr 597 |
. . . . . 6
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ ((projℎ‘𝑥)‘𝑢) ∈ ℋ) |
5 | | normcl 29487 |
. . . . . 6
⊢
(((projℎ‘𝑥)‘𝑢) ∈ ℋ →
(normℎ‘((projℎ‘𝑥)‘𝑢)) ∈ ℝ) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ (normℎ‘((projℎ‘𝑥)‘𝑢)) ∈ ℝ) |
7 | 6 | resqcld 13965 |
. . . 4
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ∈ ℝ) |
8 | 6 | sqge0d 13966 |
. . . 4
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ 0 ≤
((normℎ‘((projℎ‘𝑥)‘𝑢))↑2)) |
9 | | normge0 29488 |
. . . . . 6
⊢
(((projℎ‘𝑥)‘𝑢) ∈ ℋ → 0 ≤
(normℎ‘((projℎ‘𝑥)‘𝑢))) |
10 | 4, 9 | syl 17 |
. . . . 5
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ 0 ≤
(normℎ‘((projℎ‘𝑥)‘𝑢))) |
11 | | pjnorm 30086 |
. . . . . . 7
⊢ ((𝑥 ∈
Cℋ ∧ 𝑢 ∈ ℋ) →
(normℎ‘((projℎ‘𝑥)‘𝑢)) ≤ (normℎ‘𝑢)) |
12 | 1, 2, 11 | syl2anr 597 |
. . . . . 6
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ (normℎ‘((projℎ‘𝑥)‘𝑢)) ≤ (normℎ‘𝑢)) |
13 | | simplr 766 |
. . . . . 6
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ (normℎ‘𝑢) = 1) |
14 | 12, 13 | breqtrd 5100 |
. . . . 5
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ (normℎ‘((projℎ‘𝑥)‘𝑢)) ≤ 1) |
15 | | 2nn0 12250 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
16 | | exple1 13894 |
. . . . . 6
⊢
((((normℎ‘((projℎ‘𝑥)‘𝑢)) ∈ ℝ ∧ 0 ≤
(normℎ‘((projℎ‘𝑥)‘𝑢)) ∧
(normℎ‘((projℎ‘𝑥)‘𝑢)) ≤ 1) ∧ 2 ∈
ℕ0) →
((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ≤ 1) |
17 | 15, 16 | mpan2 688 |
. . . . 5
⊢
(((normℎ‘((projℎ‘𝑥)‘𝑢)) ∈ ℝ ∧ 0 ≤
(normℎ‘((projℎ‘𝑥)‘𝑢)) ∧
(normℎ‘((projℎ‘𝑥)‘𝑢)) ≤ 1) →
((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ≤ 1) |
18 | 6, 10, 14, 17 | syl3anc 1370 |
. . . 4
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ≤ 1) |
19 | | elicc01 13198 |
. . . 4
⊢
(((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ∈ (0[,]1) ↔
(((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ∈ ℝ ∧ 0 ≤
((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ∧
((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ≤ 1)) |
20 | 7, 8, 18, 19 | syl3anbrc 1342 |
. . 3
⊢ (((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) ∧ 𝑥 ∈ Cℋ )
→ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2) ∈ (0[,]1)) |
21 | | strlem3a.1 |
. . 3
⊢ 𝑆 = (𝑥 ∈ Cℋ
↦ ((normℎ‘((projℎ‘𝑥)‘𝑢))↑2)) |
22 | 20, 21 | fmptd 6988 |
. 2
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → 𝑆: Cℋ
⟶(0[,]1)) |
23 | | helch 29605 |
. . . 4
⊢ ℋ
∈ Cℋ |
24 | 21 | strlem2 30613 |
. . . 4
⊢ ( ℋ
∈ Cℋ → (𝑆‘ ℋ) =
((normℎ‘((projℎ‘
ℋ)‘𝑢))↑2)) |
25 | 23, 24 | ax-mp 5 |
. . 3
⊢ (𝑆‘ ℋ) =
((normℎ‘((projℎ‘
ℋ)‘𝑢))↑2) |
26 | | pjch1 30032 |
. . . . . 6
⊢ (𝑢 ∈ ℋ →
((projℎ‘ ℋ)‘𝑢) = 𝑢) |
27 | 26 | fveq2d 6778 |
. . . . 5
⊢ (𝑢 ∈ ℋ →
(normℎ‘((projℎ‘
ℋ)‘𝑢)) =
(normℎ‘𝑢)) |
28 | 27 | oveq1d 7290 |
. . . 4
⊢ (𝑢 ∈ ℋ →
((normℎ‘((projℎ‘
ℋ)‘𝑢))↑2)
= ((normℎ‘𝑢)↑2)) |
29 | | oveq1 7282 |
. . . . 5
⊢
((normℎ‘𝑢) = 1 →
((normℎ‘𝑢)↑2) = (1↑2)) |
30 | | sq1 13912 |
. . . . 5
⊢
(1↑2) = 1 |
31 | 29, 30 | eqtrdi 2794 |
. . . 4
⊢
((normℎ‘𝑢) = 1 →
((normℎ‘𝑢)↑2) = 1) |
32 | 28, 31 | sylan9eq 2798 |
. . 3
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) →
((normℎ‘((projℎ‘
ℋ)‘𝑢))↑2)
= 1) |
33 | 25, 32 | eqtrid 2790 |
. 2
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → (𝑆‘ ℋ) = 1) |
34 | | pjcjt2 30054 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
→ (𝑧 ⊆
(⊥‘𝑤) →
((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢) = (((projℎ‘𝑧)‘𝑢) +ℎ
((projℎ‘𝑤)‘𝑢)))) |
35 | 34 | imp 407 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢) = (((projℎ‘𝑧)‘𝑢) +ℎ
((projℎ‘𝑤)‘𝑢))) |
36 | 35 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
(normℎ‘((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢)) =
(normℎ‘(((projℎ‘𝑧)‘𝑢) +ℎ
((projℎ‘𝑤)‘𝑢)))) |
37 | 36 | oveq1d 7290 |
. . . . . . . . 9
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
((normℎ‘((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢))↑2) =
((normℎ‘(((projℎ‘𝑧)‘𝑢) +ℎ
((projℎ‘𝑤)‘𝑢)))↑2)) |
38 | | pjopyth 30082 |
. . . . . . . . . 10
⊢ ((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
→ (𝑧 ⊆
(⊥‘𝑤) →
((normℎ‘(((projℎ‘𝑧)‘𝑢) +ℎ
((projℎ‘𝑤)‘𝑢)))↑2) =
(((normℎ‘((projℎ‘𝑧)‘𝑢))↑2) +
((normℎ‘((projℎ‘𝑤)‘𝑢))↑2)))) |
39 | 38 | imp 407 |
. . . . . . . . 9
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
((normℎ‘(((projℎ‘𝑧)‘𝑢) +ℎ
((projℎ‘𝑤)‘𝑢)))↑2) =
(((normℎ‘((projℎ‘𝑧)‘𝑢))↑2) +
((normℎ‘((projℎ‘𝑤)‘𝑢))↑2))) |
40 | 37, 39 | eqtrd 2778 |
. . . . . . . 8
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
((normℎ‘((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢))↑2) =
(((normℎ‘((projℎ‘𝑧)‘𝑢))↑2) +
((normℎ‘((projℎ‘𝑤)‘𝑢))↑2))) |
41 | | chjcl 29719 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ )
→ (𝑧
∨ℋ 𝑤)
∈ Cℋ ) |
42 | 41 | 3adant3 1131 |
. . . . . . . . . 10
⊢ ((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
→ (𝑧
∨ℋ 𝑤)
∈ Cℋ ) |
43 | 42 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
(𝑧 ∨ℋ
𝑤) ∈
Cℋ ) |
44 | 21 | strlem2 30613 |
. . . . . . . . 9
⊢ ((𝑧 ∨ℋ 𝑤) ∈
Cℋ → (𝑆‘(𝑧 ∨ℋ 𝑤)) =
((normℎ‘((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢))↑2)) |
45 | 43, 44 | syl 17 |
. . . . . . . 8
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
(𝑆‘(𝑧 ∨ℋ 𝑤)) =
((normℎ‘((projℎ‘(𝑧 ∨ℋ 𝑤))‘𝑢))↑2)) |
46 | | 3simpa 1147 |
. . . . . . . . . 10
⊢ ((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
→ (𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
)) |
47 | 46 | adantr 481 |
. . . . . . . . 9
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
(𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
)) |
48 | 21 | strlem2 30613 |
. . . . . . . . . 10
⊢ (𝑧 ∈
Cℋ → (𝑆‘𝑧) =
((normℎ‘((projℎ‘𝑧)‘𝑢))↑2)) |
49 | 21 | strlem2 30613 |
. . . . . . . . . 10
⊢ (𝑤 ∈
Cℋ → (𝑆‘𝑤) =
((normℎ‘((projℎ‘𝑤)‘𝑢))↑2)) |
50 | 48, 49 | oveqan12d 7294 |
. . . . . . . . 9
⊢ ((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ )
→ ((𝑆‘𝑧) + (𝑆‘𝑤)) =
(((normℎ‘((projℎ‘𝑧)‘𝑢))↑2) +
((normℎ‘((projℎ‘𝑤)‘𝑢))↑2))) |
51 | 47, 50 | syl 17 |
. . . . . . . 8
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
((𝑆‘𝑧) + (𝑆‘𝑤)) =
(((normℎ‘((projℎ‘𝑧)‘𝑢))↑2) +
((normℎ‘((projℎ‘𝑤)‘𝑢))↑2))) |
52 | 40, 45, 51 | 3eqtr4d 2788 |
. . . . . . 7
⊢ (((𝑧 ∈
Cℋ ∧ 𝑤 ∈ Cℋ
∧ 𝑢 ∈ ℋ)
∧ 𝑧 ⊆
(⊥‘𝑤)) →
(𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤))) |
53 | 52 | 3exp1 1351 |
. . . . . 6
⊢ (𝑧 ∈
Cℋ → (𝑤 ∈ Cℋ
→ (𝑢 ∈ ℋ
→ (𝑧 ⊆
(⊥‘𝑤) →
(𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤)))))) |
54 | 53 | com3r 87 |
. . . . 5
⊢ (𝑢 ∈ ℋ → (𝑧 ∈
Cℋ → (𝑤 ∈ Cℋ
→ (𝑧 ⊆
(⊥‘𝑤) →
(𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤)))))) |
55 | 54 | adantr 481 |
. . . 4
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → (𝑧 ∈ Cℋ
→ (𝑤 ∈
Cℋ → (𝑧 ⊆ (⊥‘𝑤) → (𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤)))))) |
56 | 55 | ralrimdv 3105 |
. . 3
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → (𝑧 ∈ Cℋ
→ ∀𝑤 ∈
Cℋ (𝑧 ⊆ (⊥‘𝑤) → (𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤))))) |
57 | 56 | ralrimiv 3102 |
. 2
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → ∀𝑧 ∈ Cℋ
∀𝑤 ∈
Cℋ (𝑧 ⊆ (⊥‘𝑤) → (𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤)))) |
58 | | isst 30575 |
. 2
⊢ (𝑆 ∈ States ↔ (𝑆:
Cℋ ⟶(0[,]1) ∧ (𝑆‘ ℋ) = 1 ∧ ∀𝑧 ∈
Cℋ ∀𝑤 ∈ Cℋ
(𝑧 ⊆
(⊥‘𝑤) →
(𝑆‘(𝑧 ∨ℋ 𝑤)) = ((𝑆‘𝑧) + (𝑆‘𝑤))))) |
59 | 22, 33, 57, 58 | syl3anbrc 1342 |
1
⊢ ((𝑢 ∈ ℋ ∧
(normℎ‘𝑢) = 1) → 𝑆 ∈ States) |