Step | Hyp | Ref
| Expression |
1 | | chscllem3.7 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝐻‘𝑛) = (𝐻‘𝑁)) |
3 | 2 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑛 = 𝑁 →
((projℎ‘𝐴)‘(𝐻‘𝑛)) = ((projℎ‘𝐴)‘(𝐻‘𝑁))) |
4 | | chscl.6 |
. . . . . . 7
⊢ 𝐹 = (𝑛 ∈ ℕ ↦
((projℎ‘𝐴)‘(𝐻‘𝑛))) |
5 | | fvex 6201 |
. . . . . . 7
⊢
((projℎ‘𝐴)‘(𝐻‘𝑁)) ∈ V |
6 | 3, 4, 5 | fvmpt 6282 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → (𝐹‘𝑁) = ((projℎ‘𝐴)‘(𝐻‘𝑁))) |
7 | 1, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑁) = ((projℎ‘𝐴)‘(𝐻‘𝑁))) |
8 | 7 | eqcomd 2628 |
. . . 4
⊢ (𝜑 →
((projℎ‘𝐴)‘(𝐻‘𝑁)) = (𝐹‘𝑁)) |
9 | | chscl.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ Cℋ
) |
10 | | chscl.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ Cℋ
) |
11 | | chsh 28081 |
. . . . . . . . 9
⊢ (𝐵 ∈
Cℋ → 𝐵 ∈ Sℋ
) |
12 | 10, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ Sℋ
) |
13 | | chsh 28081 |
. . . . . . . . . 10
⊢ (𝐴 ∈
Cℋ → 𝐴 ∈ Sℋ
) |
14 | 9, 13 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ Sℋ
) |
15 | | shocsh 28143 |
. . . . . . . . 9
⊢ (𝐴 ∈
Sℋ → (⊥‘𝐴) ∈ Sℋ
) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (⊥‘𝐴) ∈
Sℋ ) |
17 | | chscl.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ⊆ (⊥‘𝐴)) |
18 | | shless 28218 |
. . . . . . . 8
⊢ (((𝐵 ∈
Sℋ ∧ (⊥‘𝐴) ∈ Sℋ
∧ 𝐴 ∈
Sℋ ) ∧ 𝐵 ⊆ (⊥‘𝐴)) → (𝐵 +ℋ 𝐴) ⊆ ((⊥‘𝐴) +ℋ 𝐴)) |
19 | 12, 16, 14, 17, 18 | syl31anc 1329 |
. . . . . . 7
⊢ (𝜑 → (𝐵 +ℋ 𝐴) ⊆ ((⊥‘𝐴) +ℋ 𝐴)) |
20 | | shscom 28178 |
. . . . . . . 8
⊢ ((𝐴 ∈
Sℋ ∧ 𝐵 ∈ Sℋ )
→ (𝐴
+ℋ 𝐵) =
(𝐵 +ℋ
𝐴)) |
21 | 14, 12, 20 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴)) |
22 | | shscom 28178 |
. . . . . . . 8
⊢ ((𝐴 ∈
Sℋ ∧ (⊥‘𝐴) ∈ Sℋ )
→ (𝐴
+ℋ (⊥‘𝐴)) = ((⊥‘𝐴) +ℋ 𝐴)) |
23 | 14, 16, 22 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → (𝐴 +ℋ (⊥‘𝐴)) = ((⊥‘𝐴) +ℋ 𝐴)) |
24 | 19, 21, 23 | 3sstr4d 3648 |
. . . . . 6
⊢ (𝜑 → (𝐴 +ℋ 𝐵) ⊆ (𝐴 +ℋ (⊥‘𝐴))) |
25 | | chscl.4 |
. . . . . . 7
⊢ (𝜑 → 𝐻:ℕ⟶(𝐴 +ℋ 𝐵)) |
26 | 25, 1 | ffvelrnd 6360 |
. . . . . 6
⊢ (𝜑 → (𝐻‘𝑁) ∈ (𝐴 +ℋ 𝐵)) |
27 | 24, 26 | sseldd 3604 |
. . . . 5
⊢ (𝜑 → (𝐻‘𝑁) ∈ (𝐴 +ℋ (⊥‘𝐴))) |
28 | | pjpreeq 28257 |
. . . . 5
⊢ ((𝐴 ∈
Cℋ ∧ (𝐻‘𝑁) ∈ (𝐴 +ℋ (⊥‘𝐴))) →
(((projℎ‘𝐴)‘(𝐻‘𝑁)) = (𝐹‘𝑁) ↔ ((𝐹‘𝑁) ∈ 𝐴 ∧ ∃𝑧 ∈ (⊥‘𝐴)(𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧)))) |
29 | 9, 27, 28 | syl2anc 693 |
. . . 4
⊢ (𝜑 →
(((projℎ‘𝐴)‘(𝐻‘𝑁)) = (𝐹‘𝑁) ↔ ((𝐹‘𝑁) ∈ 𝐴 ∧ ∃𝑧 ∈ (⊥‘𝐴)(𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧)))) |
30 | 8, 29 | mpbid 222 |
. . 3
⊢ (𝜑 → ((𝐹‘𝑁) ∈ 𝐴 ∧ ∃𝑧 ∈ (⊥‘𝐴)(𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) |
31 | 30 | simprd 479 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ (⊥‘𝐴)(𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧)) |
32 | 14 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐴 ∈ Sℋ
) |
33 | 16 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (⊥‘𝐴) ∈ Sℋ
) |
34 | | ocin 28155 |
. . . . . 6
⊢ (𝐴 ∈
Sℋ → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ) |
35 | 14, 34 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ) |
36 | 35 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ) |
37 | | chscllem3.8 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ 𝐴) |
38 | 37 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐶 ∈ 𝐴) |
39 | 17 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐵 ⊆ (⊥‘𝐴)) |
40 | | chscllem3.9 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝐵) |
41 | 40 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐷 ∈ 𝐵) |
42 | 39, 41 | sseldd 3604 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐷 ∈ (⊥‘𝐴)) |
43 | | chscl.5 |
. . . . . . 7
⊢ (𝜑 → 𝐻 ⇝𝑣 𝑢) |
44 | 9, 10, 17, 25, 43, 4 | chscllem1 28496 |
. . . . . 6
⊢ (𝜑 → 𝐹:ℕ⟶𝐴) |
45 | 44, 1 | ffvelrnd 6360 |
. . . . 5
⊢ (𝜑 → (𝐹‘𝑁) ∈ 𝐴) |
46 | 45 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐹‘𝑁) ∈ 𝐴) |
47 | | simprl 794 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝑧 ∈ (⊥‘𝐴)) |
48 | | chscllem3.10 |
. . . . . 6
⊢ (𝜑 → (𝐻‘𝑁) = (𝐶 +ℎ 𝐷)) |
49 | 48 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐻‘𝑁) = (𝐶 +ℎ 𝐷)) |
50 | | simprr 796 |
. . . . 5
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧)) |
51 | 49, 50 | eqtr3d 2658 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐶 +ℎ 𝐷) = ((𝐹‘𝑁) +ℎ 𝑧)) |
52 | 32, 33, 36, 38, 42, 46, 47, 51 | shuni 28159 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → (𝐶 = (𝐹‘𝑁) ∧ 𝐷 = 𝑧)) |
53 | 52 | simpld 475 |
. 2
⊢ ((𝜑 ∧ (𝑧 ∈ (⊥‘𝐴) ∧ (𝐻‘𝑁) = ((𝐹‘𝑁) +ℎ 𝑧))) → 𝐶 = (𝐹‘𝑁)) |
54 | 31, 53 | rexlimddv 3035 |
1
⊢ (𝜑 → 𝐶 = (𝐹‘𝑁)) |