Step | Hyp | Ref
| Expression |
1 | | chscllem3.7 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | 2fveq3 6722 |
. . . . . . 7
⊢ (𝑛 = 𝑁 →
((projℎ‘𝐴)‘(𝐻‘𝑛)) = ((projℎ‘𝐴)‘(𝐻‘𝑁))) |
3 | | chscl.6 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ℕ ↦
((projℎ‘𝐴)‘(𝐻‘𝑛))) |
4 | | fvex 6730 |
. . . . . . 7
⊢
((projℎ‘𝐴)‘(𝐻‘𝑁)) ∈ V |
5 | 2, 3, 4 | fvmpt 6818 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) = ((projℎ‘𝐴)‘(𝐻‘𝑁))) |
6 | 1, 5 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑁) = ((projℎ‘𝐴)‘(𝐻‘𝑁))) |
7 | 6 | eqcomd 2743 |
. . . 4
⊢ (𝜑 →
((projℎ‘𝐴)‘(𝐻‘𝑁)) = (𝐹‘𝑁)) |
8 | | chscl.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ Cℋ
) |
9 | | chscl.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ Cℋ
) |
10 | | chsh 29305 |
. . . . . . . . 9
⊢ (𝐵 ∈
Cℋ → 𝐵 ∈ Sℋ
) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ Sℋ
) |
12 | | chsh 29305 |
. . . . . . . . . 10
⊢ (𝐴 ∈
Cℋ → 𝐴 ∈ Sℋ
) |
13 | 8, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ Sℋ
) |
14 | | shocsh 29365 |
. . . . . . . . 9
⊢ (𝐴 ∈
Sℋ → (⊥‘𝐴) ∈ Sℋ
) |
15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (⊥‘𝐴) ∈
Sℋ ) |
16 | | chscl.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴)) |
17 | | shless 29440 |
. . . . . . . 8
⊢ (((𝐵 ∈
Sℋ ∧ (⊥‘𝐴) ∈ Sℋ
∧ 𝐴 ∈
Sℋ ) ∧ 𝐵 ⊆ (⊥‘𝐴)) → (𝐵 +ℋ 𝐴) ⊆ ((⊥‘𝐴) +ℋ 𝐴)) |
18 | 11, 15, 13, 16, 17 | syl31anc 1375 |
. . . . . . 7
⊢ (𝜑 → (𝐵 +ℋ 𝐴) ⊆ ((⊥‘𝐴) +ℋ 𝐴)) |
19 | | shscom 29400 |
. . . . . . . 8
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐴
+ℋ 𝐵) =
(𝐵 +ℋ
𝐴)) |
20 | 13, 11, 19 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴)) |
21 | | shscom 29400 |
. . . . . . . 8
⊢ ((𝐴 ∈
Sℋ ∧ (⊥‘𝐴) ∈ Sℋ )
→ (𝐴
+ℋ (⊥‘𝐴)) = ((⊥‘𝐴) +ℋ 𝐴)) |
22 | 13, 15, 21 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → (𝐴 +ℋ (⊥‘𝐴)) = ((⊥‘𝐴) +ℋ 𝐴)) |
23 | 18, 20, 22 | 3sstr4d 3948 |
. . . . . 6
⊢ (𝜑 → (𝐴 +ℋ 𝐵) ⊆ (𝐴 +ℋ (⊥‘𝐴))) |
24 | | chscl.4 |
. . . . . . 7
⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵)) |
25 | 24, 1 | ffvelrnd 6905 |
. . . . . 6
⊢ (𝜑 → (𝐻‘𝑁) ∈ (𝐴 +ℋ 𝐵)) |
26 | 23, 25 | sseldd 3902 |
. . . . 5
⊢ (𝜑 → (𝐻‘𝑁) ∈ (𝐴 +ℋ (⊥‘𝐴))) |
27 | | pjpreeq 29479 |
. . . . 5
⊢ ((𝐴 ∈
Cℋ ∧ (𝐻‘𝑁) ∈ (𝐴 +ℋ (⊥‘𝐴))) →
(((projℎ‘𝐴)‘(𝐻‘𝑁)) = (𝐹‘𝑁) ↔ ((𝐹‘𝑁) ∈ 𝐴 ∧ ∃𝑧 ∈ (⊥‘𝐴)(𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧)))) |
28 | 8, 26, 27 | syl2anc 587 |
. . . 4
⊢ (𝜑 →
(((projℎ‘𝐴)‘(𝐻‘𝑁)) = (𝐹‘𝑁) ↔ ((𝐹‘𝑁) ∈ 𝐴 ∧ ∃𝑧 ∈ (⊥‘𝐴)(𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧)))) |
29 | 7, 28 | mpbid 235 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑁) ∈ 𝐴 ∧ ∃𝑧 ∈ (⊥‘𝐴)(𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) |
30 | 29 | simprd 499 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ (⊥‘𝐴)(𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧)) |
31 | 13 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐴 ∈ Sℋ
) |
32 | 15 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (⊥‘𝐴) ∈ Sℋ
) |
33 | | ocin 29377 |
. . . . . 6
⊢ (𝐴 ∈
Sℋ → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ) |
34 | 13, 33 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ) |
35 | 34 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ) |
36 | | chscllem3.8 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
37 | 36 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐶 ∈ 𝐴) |
38 | 16 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐵 ⊆ (⊥‘𝐴)) |
39 | | chscllem3.9 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝐵) |
40 | 39 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐷 ∈ 𝐵) |
41 | 38, 40 | sseldd 3902 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐷 ∈ (⊥‘𝐴)) |
42 | | chscl.5 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢) |
43 | 8, 9, 16, 24, 42, 3 | chscllem1 29718 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶𝐴) |
44 | 43, 1 | ffvelrnd 6905 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑁) ∈ 𝐴) |
45 | 44 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐹‘𝑁) ∈ 𝐴) |
46 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝑧 ∈ (⊥‘𝐴)) |
47 | | chscllem3.10 |
. . . . . 6
⊢ (𝜑 → (𝐻‘𝑁) = (𝐶 +ℎ 𝐷)) |
48 | 47 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐻‘𝑁) = (𝐶 +ℎ 𝐷)) |
49 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧)) |
50 | 48, 49 | eqtr3d 2779 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐶 +ℎ 𝐷) = ((𝐹‘𝑁) +ℎ 𝑧)) |
51 | 31, 32, 35, 37, 41, 45, 46, 50 | shuni 29381 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐶 = (𝐹‘𝑁) ∧ 𝐷 = 𝑧)) |
52 | 51 | simpld 498 |
. 2
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐶 = (𝐹‘𝑁)) |
53 | 30, 52 | rexlimddv 3210 |
1
⊢ (𝜑 → 𝐶 = (𝐹‘𝑁)) |