| Step | Hyp | Ref
| Expression |
| 1 | | chscllem3.7 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 2 | | 2fveq3 6911 |
. . . . . . 7
⊢ (𝑛 = 𝑁 →
((projℎ‘𝐴)‘(𝐻‘𝑛)) = ((projℎ‘𝐴)‘(𝐻‘𝑁))) |
| 3 | | chscl.6 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ℕ ↦
((projℎ‘𝐴)‘(𝐻‘𝑛))) |
| 4 | | fvex 6919 |
. . . . . . 7
⊢
((projℎ‘𝐴)‘(𝐻‘𝑁)) ∈ V |
| 5 | 2, 3, 4 | fvmpt 7016 |
. . . . . 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 31243 |
. . . . . . . . 9
⊢ (𝐵 ∈
Cℋ → 𝐵 ∈ Sℋ
) |
| 11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ Sℋ
) |
| 12 | | chsh 31243 |
. . . . . . . . . 10
⊢ (𝐴 ∈
Cℋ → 𝐴 ∈ Sℋ
) |
| 13 | 8, 12 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ Sℋ
) |
| 14 | | shocsh 31303 |
. . . . . . . . 9
⊢ (𝐴 ∈
Sℋ → (⊥‘𝐴) ∈ Sℋ
) |
| 15 | 13, 14 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (⊥‘𝐴) ∈
Sℋ ) |
| 16 | | chscl.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴)) |
| 17 | | shless 31378 |
. . . . . . . 8
⊢ (((𝐵 ∈
Sℋ ∧ (⊥‘𝐴) ∈ Sℋ
∧ 𝐴 ∈
Sℋ ) ∧ 𝐵 ⊆ (⊥‘𝐴)) → (𝐵 +ℋ 𝐴) ⊆ ((⊥‘𝐴) +ℋ 𝐴)) |
| 18 | 11, 15, 13, 16, 17 | syl31anc 1375 |
. . . . . . 7
⊢ (𝜑 → (𝐵 +ℋ 𝐴) ⊆ ((⊥‘𝐴) +ℋ 𝐴)) |
| 19 | | shscom 31338 |
. . . . . . . 8
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐴
+ℋ 𝐵) =
(𝐵 +ℋ
𝐴)) |
| 20 | 13, 11, 19 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴)) |
| 21 | | shscom 31338 |
. . . . . . . 8
⊢ ((𝐴 ∈
Sℋ ∧ (⊥‘𝐴) ∈ Sℋ )
→ (𝐴
+ℋ (⊥‘𝐴)) = ((⊥‘𝐴) +ℋ 𝐴)) |
| 22 | 13, 15, 21 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → (𝐴 +ℋ (⊥‘𝐴)) = ((⊥‘𝐴) +ℋ 𝐴)) |
| 23 | 18, 20, 22 | 3sstr4d 4039 |
. . . . . 6
⊢ (𝜑 → (𝐴 +ℋ 𝐵) ⊆ (𝐴 +ℋ (⊥‘𝐴))) |
| 24 | | chscl.4 |
. . . . . . 7
⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵)) |
| 25 | 24, 1 | ffvelcdmd 7105 |
. . . . . 6
⊢ (𝜑 → (𝐻‘𝑁) ∈ (𝐴 +ℋ 𝐵)) |
| 26 | 23, 25 | sseldd 3984 |
. . . . 5
⊢ (𝜑 → (𝐻‘𝑁) ∈ (𝐴 +ℋ (⊥‘𝐴))) |
| 27 | | pjpreeq 31417 |
. . . . 5
⊢ ((𝐴 ∈
Cℋ ∧ (𝐻‘𝑁) ∈ (𝐴 +ℋ (⊥‘𝐴))) →
(((projℎ‘𝐴)‘(𝐻‘𝑁)) = (𝐹‘𝑁) ↔ ((𝐹‘𝑁) ∈ 𝐴 ∧ ∃𝑧 ∈ (⊥‘𝐴)(𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧)))) |
| 28 | 8, 26, 27 | syl2anc 584 |
. . . 4
⊢ (𝜑 →
(((projℎ‘𝐴)‘(𝐻‘𝑁)) = (𝐹‘𝑁) ↔ ((𝐹‘𝑁) ∈ 𝐴 ∧ ∃𝑧 ∈ (⊥‘𝐴)(𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧)))) |
| 29 | 7, 28 | mpbid 232 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑁) ∈ 𝐴 ∧ ∃𝑧 ∈ (⊥‘𝐴)(𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) |
| 30 | 29 | simprd 495 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ (⊥‘𝐴)(𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧)) |
| 31 | 13 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐴 ∈ Sℋ
) |
| 32 | 15 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (⊥‘𝐴) ∈ Sℋ
) |
| 33 | | ocin 31315 |
. . . . . 6
⊢ (𝐴 ∈
Sℋ → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ) |
| 34 | 13, 33 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ) |
| 35 | 34 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ) |
| 36 | | chscllem3.8 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
| 37 | 36 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐶 ∈ 𝐴) |
| 38 | 16 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐵 ⊆ (⊥‘𝐴)) |
| 39 | | chscllem3.9 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝐵) |
| 40 | 39 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐷 ∈ 𝐵) |
| 41 | 38, 40 | sseldd 3984 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐷 ∈ (⊥‘𝐴)) |
| 42 | | chscl.5 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢) |
| 43 | 8, 9, 16, 24, 42, 3 | chscllem1 31656 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶𝐴) |
| 44 | 43, 1 | ffvelcdmd 7105 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑁) ∈ 𝐴) |
| 45 | 44 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐹‘𝑁) ∈ 𝐴) |
| 46 | | simprl 771 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝑧 ∈ (⊥‘𝐴)) |
| 47 | | chscllem3.10 |
. . . . . 6
⊢ (𝜑 → (𝐻‘𝑁) = (𝐶 +ℎ 𝐷)) |
| 48 | 47 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐻‘𝑁) = (𝐶 +ℎ 𝐷)) |
| 49 | | simprr 773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧)) |
| 50 | 48, 49 | eqtr3d 2779 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐶 +ℎ 𝐷) = ((𝐹‘𝑁) +ℎ 𝑧)) |
| 51 | 31, 32, 35, 37, 41, 45, 46, 50 | shuni 31319 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐶 = (𝐹‘𝑁) ∧ 𝐷 = 𝑧)) |
| 52 | 51 | simpld 494 |
. 2
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐶 = (𝐹‘𝑁)) |
| 53 | 30, 52 | rexlimddv 3161 |
1
⊢ (𝜑 → 𝐶 = (𝐹‘𝑁)) |