Proof of Theorem pjclem1
| Step | Hyp | Ref
| Expression |
| 1 | | pjclem1.1 |
. . . . . 6
⊢ 𝐺 ∈
Cℋ |
| 2 | | pjclem1.2 |
. . . . . 6
⊢ 𝐻 ∈
Cℋ |
| 3 | 1, 2 | cmbri 31609 |
. . . . 5
⊢ (𝐺 𝐶ℋ
𝐻 ↔ 𝐺 = ((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻)))) |
| 4 | | fveq2 6906 |
. . . . 5
⊢ (𝐺 = ((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻))) →
(projℎ‘𝐺) = (projℎ‘((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻))))) |
| 5 | 3, 4 | sylbi 217 |
. . . 4
⊢ (𝐺 𝐶ℋ
𝐻 →
(projℎ‘𝐺) = (projℎ‘((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻))))) |
| 6 | | inss2 4238 |
. . . . . . . 8
⊢ (𝐺 ∩ 𝐻) ⊆ 𝐻 |
| 7 | 1 | choccli 31326 |
. . . . . . . . . 10
⊢
(⊥‘𝐺)
∈ Cℋ |
| 8 | 2, 7 | chub2i 31489 |
. . . . . . . . 9
⊢ 𝐻 ⊆ ((⊥‘𝐺) ∨ℋ 𝐻) |
| 9 | 1, 2 | chdmm3i 31498 |
. . . . . . . . 9
⊢
(⊥‘(𝐺
∩ (⊥‘𝐻))) =
((⊥‘𝐺)
∨ℋ 𝐻) |
| 10 | 8, 9 | sseqtrri 4033 |
. . . . . . . 8
⊢ 𝐻 ⊆ (⊥‘(𝐺 ∩ (⊥‘𝐻))) |
| 11 | 6, 10 | sstri 3993 |
. . . . . . 7
⊢ (𝐺 ∩ 𝐻) ⊆ (⊥‘(𝐺 ∩ (⊥‘𝐻))) |
| 12 | 1, 2 | chincli 31479 |
. . . . . . . 8
⊢ (𝐺 ∩ 𝐻) ∈
Cℋ |
| 13 | 2 | choccli 31326 |
. . . . . . . . 9
⊢
(⊥‘𝐻)
∈ Cℋ |
| 14 | 1, 13 | chincli 31479 |
. . . . . . . 8
⊢ (𝐺 ∩ (⊥‘𝐻)) ∈
Cℋ |
| 15 | 12, 14 | pjscji 32189 |
. . . . . . 7
⊢ ((𝐺 ∩ 𝐻) ⊆ (⊥‘(𝐺 ∩ (⊥‘𝐻))) →
(projℎ‘((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻)))) =
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) |
| 16 | 11, 15 | ax-mp 5 |
. . . . . 6
⊢
(projℎ‘((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻)))) =
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻)))) |
| 17 | 16 | eqeq2i 2750 |
. . . . 5
⊢
((projℎ‘𝐺) = (projℎ‘((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻)))) ↔
(projℎ‘𝐺) = ((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) |
| 18 | | coeq2 5869 |
. . . . . 6
⊢
((projℎ‘𝐺) = ((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻)))) →
((projℎ‘𝐻) ∘
(projℎ‘𝐺)) = ((projℎ‘𝐻) ∘
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻)))))) |
| 19 | 12 | pjfi 31723 |
. . . . . . . . . 10
⊢
(projℎ‘(𝐺 ∩ 𝐻)): ℋ⟶ ℋ |
| 20 | 14 | pjfi 31723 |
. . . . . . . . . 10
⊢
(projℎ‘(𝐺 ∩ (⊥‘𝐻))): ℋ⟶
ℋ |
| 21 | 2, 19, 20 | pjsdii 32174 |
. . . . . . . . 9
⊢
((projℎ‘𝐻) ∘
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) =
(((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ 𝐻))) +op
((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) |
| 22 | 12, 2 | pjss1coi 32182 |
. . . . . . . . . . 11
⊢ ((𝐺 ∩ 𝐻) ⊆ 𝐻 ↔
((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ 𝐻))) = (projℎ‘(𝐺 ∩ 𝐻))) |
| 23 | 6, 22 | mpbi 230 |
. . . . . . . . . 10
⊢
((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ 𝐻))) = (projℎ‘(𝐺 ∩ 𝐻)) |
| 24 | 2, 14 | pjorthcoi 32188 |
. . . . . . . . . . 11
⊢ (𝐻 ⊆ (⊥‘(𝐺 ∩ (⊥‘𝐻))) →
((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ (⊥‘𝐻)))) = 0hop ) |
| 25 | 10, 24 | ax-mp 5 |
. . . . . . . . . 10
⊢
((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ (⊥‘𝐻)))) = 0hop |
| 26 | 23, 25 | oveq12i 7443 |
. . . . . . . . 9
⊢
(((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ 𝐻))) +op
((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) =
((projℎ‘(𝐺 ∩ 𝐻)) +op 0hop
) |
| 27 | 19 | hoaddridi 31805 |
. . . . . . . . 9
⊢
((projℎ‘(𝐺 ∩ 𝐻)) +op 0hop ) =
(projℎ‘(𝐺 ∩ 𝐻)) |
| 28 | 21, 26, 27 | 3eqtri 2769 |
. . . . . . . 8
⊢
((projℎ‘𝐻) ∘
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) =
(projℎ‘(𝐺 ∩ 𝐻)) |
| 29 | 28 | eqeq2i 2750 |
. . . . . . 7
⊢
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) = ((projℎ‘𝐻) ∘
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) ↔
((projℎ‘𝐻) ∘
(projℎ‘𝐺)) = (projℎ‘(𝐺 ∩ 𝐻))) |
| 30 | | coeq2 5869 |
. . . . . . . 8
⊢
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) = (projℎ‘(𝐺 ∩ 𝐻)) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) = ((projℎ‘𝐺) ∘
(projℎ‘(𝐺 ∩ 𝐻)))) |
| 31 | | inss1 4237 |
. . . . . . . . 9
⊢ (𝐺 ∩ 𝐻) ⊆ 𝐺 |
| 32 | 12, 1 | pjss1coi 32182 |
. . . . . . . . 9
⊢ ((𝐺 ∩ 𝐻) ⊆ 𝐺 ↔
((projℎ‘𝐺) ∘
(projℎ‘(𝐺 ∩ 𝐻))) = (projℎ‘(𝐺 ∩ 𝐻))) |
| 33 | 31, 32 | mpbi 230 |
. . . . . . . 8
⊢
((projℎ‘𝐺) ∘
(projℎ‘(𝐺 ∩ 𝐻))) = (projℎ‘(𝐺 ∩ 𝐻)) |
| 34 | 30, 33 | eqtrdi 2793 |
. . . . . . 7
⊢
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) = (projℎ‘(𝐺 ∩ 𝐻)) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) = (projℎ‘(𝐺 ∩ 𝐻))) |
| 35 | 29, 34 | sylbi 217 |
. . . . . 6
⊢
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) = ((projℎ‘𝐻) ∘
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) = (projℎ‘(𝐺 ∩ 𝐻))) |
| 36 | 18, 35 | syl 17 |
. . . . 5
⊢
((projℎ‘𝐺) = ((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻)))) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) = (projℎ‘(𝐺 ∩ 𝐻))) |
| 37 | 17, 36 | sylbi 217 |
. . . 4
⊢
((projℎ‘𝐺) = (projℎ‘((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻)))) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) = (projℎ‘(𝐺 ∩ 𝐻))) |
| 38 | 5, 37 | syl 17 |
. . 3
⊢ (𝐺 𝐶ℋ
𝐻 →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) = (projℎ‘(𝐺 ∩ 𝐻))) |
| 39 | 1, 2 | cmcm3i 31613 |
. . . . 5
⊢ (𝐺 𝐶ℋ
𝐻 ↔
(⊥‘𝐺)
𝐶ℋ 𝐻) |
| 40 | 7, 2 | cmbri 31609 |
. . . . 5
⊢
((⊥‘𝐺)
𝐶ℋ 𝐻 ↔ (⊥‘𝐺) = (((⊥‘𝐺) ∩ 𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻)))) |
| 41 | 39, 40 | bitri 275 |
. . . 4
⊢ (𝐺 𝐶ℋ
𝐻 ↔
(⊥‘𝐺) =
(((⊥‘𝐺) ∩
𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻)))) |
| 42 | | fveq2 6906 |
. . . . 5
⊢
((⊥‘𝐺) =
(((⊥‘𝐺) ∩
𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻))) →
(projℎ‘(⊥‘𝐺)) =
(projℎ‘(((⊥‘𝐺) ∩ 𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻))))) |
| 43 | | inss2 4238 |
. . . . . . . . 9
⊢
((⊥‘𝐺)
∩ 𝐻) ⊆ 𝐻 |
| 44 | 2, 1 | chub2i 31489 |
. . . . . . . . . 10
⊢ 𝐻 ⊆ (𝐺 ∨ℋ 𝐻) |
| 45 | 1, 2 | chdmm4i 31499 |
. . . . . . . . . 10
⊢
(⊥‘((⊥‘𝐺) ∩ (⊥‘𝐻))) = (𝐺 ∨ℋ 𝐻) |
| 46 | 44, 45 | sseqtrri 4033 |
. . . . . . . . 9
⊢ 𝐻 ⊆
(⊥‘((⊥‘𝐺) ∩ (⊥‘𝐻))) |
| 47 | 43, 46 | sstri 3993 |
. . . . . . . 8
⊢
((⊥‘𝐺)
∩ 𝐻) ⊆
(⊥‘((⊥‘𝐺) ∩ (⊥‘𝐻))) |
| 48 | 7, 2 | chincli 31479 |
. . . . . . . . 9
⊢
((⊥‘𝐺)
∩ 𝐻) ∈
Cℋ |
| 49 | 7, 13 | chincli 31479 |
. . . . . . . . 9
⊢
((⊥‘𝐺)
∩ (⊥‘𝐻))
∈ Cℋ |
| 50 | 48, 49 | pjscji 32189 |
. . . . . . . 8
⊢
(((⊥‘𝐺)
∩ 𝐻) ⊆
(⊥‘((⊥‘𝐺) ∩ (⊥‘𝐻))) →
(projℎ‘(((⊥‘𝐺) ∩ 𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻)))) =
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) |
| 51 | 47, 50 | ax-mp 5 |
. . . . . . 7
⊢
(projℎ‘(((⊥‘𝐺) ∩ 𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻)))) =
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻)))) |
| 52 | 51 | eqeq2i 2750 |
. . . . . 6
⊢
((projℎ‘(⊥‘𝐺)) =
(projℎ‘(((⊥‘𝐺) ∩ 𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻)))) ↔
(projℎ‘(⊥‘𝐺)) =
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) |
| 53 | | coeq2 5869 |
. . . . . . 7
⊢
((projℎ‘(⊥‘𝐺)) =
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻)))) →
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))) = ((projℎ‘𝐻) ∘
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻)))))) |
| 54 | 48 | pjfi 31723 |
. . . . . . . . . . 11
⊢
(projℎ‘((⊥‘𝐺) ∩ 𝐻)): ℋ⟶ ℋ |
| 55 | 49 | pjfi 31723 |
. . . . . . . . . . 11
⊢
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))): ℋ⟶
ℋ |
| 56 | 2, 54, 55 | pjsdii 32174 |
. . . . . . . . . 10
⊢
((projℎ‘𝐻) ∘
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) =
(((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) +op
((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) |
| 57 | 48, 2 | pjss1coi 32182 |
. . . . . . . . . . . 12
⊢
(((⊥‘𝐺)
∩ 𝐻) ⊆ 𝐻 ↔
((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) |
| 58 | 43, 57 | mpbi 230 |
. . . . . . . . . . 11
⊢
((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻)) |
| 59 | 2, 49 | pjorthcoi 32188 |
. . . . . . . . . . . 12
⊢ (𝐻 ⊆
(⊥‘((⊥‘𝐺) ∩ (⊥‘𝐻))) →
((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻)))) = 0hop ) |
| 60 | 46, 59 | ax-mp 5 |
. . . . . . . . . . 11
⊢
((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻)))) = 0hop |
| 61 | 58, 60 | oveq12i 7443 |
. . . . . . . . . 10
⊢
(((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) +op
((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) =
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op 0hop
) |
| 62 | 54 | hoaddridi 31805 |
. . . . . . . . . 10
⊢
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op 0hop ) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻)) |
| 63 | 56, 61, 62 | 3eqtri 2769 |
. . . . . . . . 9
⊢
((projℎ‘𝐻) ∘
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻)) |
| 64 | 63 | eqeq2i 2750 |
. . . . . . . 8
⊢
(((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))) = ((projℎ‘𝐻) ∘
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) ↔
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) |
| 65 | | coeq2 5869 |
. . . . . . . . 9
⊢
(((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻)) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) = ((projℎ‘𝐺) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻)))) |
| 66 | 1, 13 | chub1i 31488 |
. . . . . . . . . . 11
⊢ 𝐺 ⊆ (𝐺 ∨ℋ (⊥‘𝐻)) |
| 67 | 1, 2 | chdmm2i 31497 |
. . . . . . . . . . 11
⊢
(⊥‘((⊥‘𝐺) ∩ 𝐻)) = (𝐺 ∨ℋ (⊥‘𝐻)) |
| 68 | 66, 67 | sseqtrri 4033 |
. . . . . . . . . 10
⊢ 𝐺 ⊆
(⊥‘((⊥‘𝐺) ∩ 𝐻)) |
| 69 | 1, 48 | pjorthcoi 32188 |
. . . . . . . . . 10
⊢ (𝐺 ⊆
(⊥‘((⊥‘𝐺) ∩ 𝐻)) →
((projℎ‘𝐺) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) = 0hop ) |
| 70 | 68, 69 | ax-mp 5 |
. . . . . . . . 9
⊢
((projℎ‘𝐺) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) = 0hop |
| 71 | 65, 70 | eqtrdi 2793 |
. . . . . . . 8
⊢
(((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻)) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) = 0hop ) |
| 72 | 64, 71 | sylbi 217 |
. . . . . . 7
⊢
(((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))) = ((projℎ‘𝐻) ∘
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) = 0hop ) |
| 73 | 53, 72 | syl 17 |
. . . . . 6
⊢
((projℎ‘(⊥‘𝐺)) =
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻)))) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) = 0hop ) |
| 74 | 52, 73 | sylbi 217 |
. . . . 5
⊢
((projℎ‘(⊥‘𝐺)) =
(projℎ‘(((⊥‘𝐺) ∩ 𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻)))) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) = 0hop ) |
| 75 | 42, 74 | syl 17 |
. . . 4
⊢
((⊥‘𝐺) =
(((⊥‘𝐺) ∩
𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻))) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) = 0hop ) |
| 76 | 41, 75 | sylbi 217 |
. . 3
⊢ (𝐺 𝐶ℋ
𝐻 →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) = 0hop ) |
| 77 | 38, 76 | oveq12d 7449 |
. 2
⊢ (𝐺 𝐶ℋ
𝐻 →
(((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) +op
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))))) =
((projℎ‘(𝐺 ∩ 𝐻)) +op 0hop
)) |
| 78 | | df-iop 31768 |
. . . . . . 7
⊢
Iop = (projℎ‘ ℋ) |
| 79 | 78 | coeq2i 5871 |
. . . . . 6
⊢
((projℎ‘𝐻) ∘ Iop ) =
((projℎ‘𝐻) ∘ (projℎ‘
ℋ)) |
| 80 | 2 | pjfi 31723 |
. . . . . . 7
⊢
(projℎ‘𝐻): ℋ⟶ ℋ |
| 81 | 80 | hoid1i 31808 |
. . . . . 6
⊢
((projℎ‘𝐻) ∘ Iop ) =
(projℎ‘𝐻) |
| 82 | 79, 81 | eqtr3i 2767 |
. . . . 5
⊢
((projℎ‘𝐻) ∘ (projℎ‘
ℋ)) = (projℎ‘𝐻) |
| 83 | 1 | pjtoi 32198 |
. . . . . . 7
⊢
((projℎ‘𝐺) +op
(projℎ‘(⊥‘𝐺))) = (projℎ‘
ℋ) |
| 84 | 83 | coeq2i 5871 |
. . . . . 6
⊢
((projℎ‘𝐻) ∘
((projℎ‘𝐺) +op
(projℎ‘(⊥‘𝐺)))) = ((projℎ‘𝐻) ∘
(projℎ‘ ℋ)) |
| 85 | 1 | pjfi 31723 |
. . . . . . 7
⊢
(projℎ‘𝐺): ℋ⟶ ℋ |
| 86 | 7 | pjfi 31723 |
. . . . . . 7
⊢
(projℎ‘(⊥‘𝐺)): ℋ⟶ ℋ |
| 87 | 2, 85, 86 | pjsdii 32174 |
. . . . . 6
⊢
((projℎ‘𝐻) ∘
((projℎ‘𝐺) +op
(projℎ‘(⊥‘𝐺)))) =
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) +op
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) |
| 88 | 84, 87 | eqtr3i 2767 |
. . . . 5
⊢
((projℎ‘𝐻) ∘ (projℎ‘
ℋ)) = (((projℎ‘𝐻) ∘
(projℎ‘𝐺)) +op
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) |
| 89 | 82, 88 | eqtr3i 2767 |
. . . 4
⊢
(projℎ‘𝐻) = (((projℎ‘𝐻) ∘
(projℎ‘𝐺)) +op
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) |
| 90 | 89 | coeq2i 5871 |
. . 3
⊢
((projℎ‘𝐺) ∘
(projℎ‘𝐻)) = ((projℎ‘𝐺) ∘
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) +op
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))))) |
| 91 | 80, 85 | hocofi 31785 |
. . . 4
⊢
((projℎ‘𝐻) ∘
(projℎ‘𝐺)): ℋ⟶ ℋ |
| 92 | 80, 86 | hocofi 31785 |
. . . 4
⊢
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))): ℋ⟶
ℋ |
| 93 | 1, 91, 92 | pjsdii 32174 |
. . 3
⊢
((projℎ‘𝐺) ∘
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) +op
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))))) =
(((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) +op
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))))) |
| 94 | 90, 93 | eqtr2i 2766 |
. 2
⊢
(((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) +op
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))))) =
((projℎ‘𝐺) ∘
(projℎ‘𝐻)) |
| 95 | 77, 94, 27 | 3eqtr3g 2800 |
1
⊢ (𝐺 𝐶ℋ
𝐻 →
((projℎ‘𝐺) ∘
(projℎ‘𝐻)) = (projℎ‘(𝐺 ∩ 𝐻))) |