Proof of Theorem pjclem1
Step | Hyp | Ref
| Expression |
1 | | pjclem1.1 |
. . . . . 6
⊢ 𝐺 ∈
Cℋ |
2 | | pjclem1.2 |
. . . . . 6
⊢ 𝐻 ∈
Cℋ |
3 | 1, 2 | cmbri 29538 |
. . . . 5
⊢ (𝐺 𝐶ℋ
𝐻 ↔ 𝐺 = ((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻)))) |
4 | | fveq2 6687 |
. . . . 5
⊢ (𝐺 = ((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻))) →
(projℎ‘𝐺) = (projℎ‘((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻))))) |
5 | 3, 4 | sylbi 220 |
. . . 4
⊢ (𝐺 𝐶ℋ
𝐻 →
(projℎ‘𝐺) = (projℎ‘((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻))))) |
6 | | inss2 4130 |
. . . . . . . 8
⊢ (𝐺 ∩ 𝐻) ⊆ 𝐻 |
7 | 1 | choccli 29255 |
. . . . . . . . . 10
⊢
(⊥‘𝐺)
∈ Cℋ |
8 | 2, 7 | chub2i 29418 |
. . . . . . . . 9
⊢ 𝐻 ⊆ ((⊥‘𝐺) ∨ℋ 𝐻) |
9 | 1, 2 | chdmm3i 29427 |
. . . . . . . . 9
⊢
(⊥‘(𝐺
∩ (⊥‘𝐻))) =
((⊥‘𝐺)
∨ℋ 𝐻) |
10 | 8, 9 | sseqtrri 3924 |
. . . . . . . 8
⊢ 𝐻 ⊆ (⊥‘(𝐺 ∩ (⊥‘𝐻))) |
11 | 6, 10 | sstri 3896 |
. . . . . . 7
⊢ (𝐺 ∩ 𝐻) ⊆ (⊥‘(𝐺 ∩ (⊥‘𝐻))) |
12 | 1, 2 | chincli 29408 |
. . . . . . . 8
⊢ (𝐺 ∩ 𝐻) ∈
Cℋ |
13 | 2 | choccli 29255 |
. . . . . . . . 9
⊢
(⊥‘𝐻)
∈ Cℋ |
14 | 1, 13 | chincli 29408 |
. . . . . . . 8
⊢ (𝐺 ∩ (⊥‘𝐻)) ∈
Cℋ |
15 | 12, 14 | pjscji 30118 |
. . . . . . 7
⊢ ((𝐺 ∩ 𝐻) ⊆ (⊥‘(𝐺 ∩ (⊥‘𝐻))) →
(projℎ‘((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻)))) =
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) |
16 | 11, 15 | ax-mp 5 |
. . . . . 6
⊢
(projℎ‘((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻)))) =
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻)))) |
17 | 16 | eqeq2i 2752 |
. . . . 5
⊢
((projℎ‘𝐺) = (projℎ‘((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻)))) ↔
(projℎ‘𝐺) = ((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) |
18 | | coeq2 5711 |
. . . . . 6
⊢
((projℎ‘𝐺) = ((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻)))) →
((projℎ‘𝐻) ∘
(projℎ‘𝐺)) = ((projℎ‘𝐻) ∘
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻)))))) |
19 | 12 | pjfi 29652 |
. . . . . . . . . 10
⊢
(projℎ‘(𝐺 ∩ 𝐻)): ℋ⟶ ℋ |
20 | 14 | pjfi 29652 |
. . . . . . . . . 10
⊢
(projℎ‘(𝐺 ∩ (⊥‘𝐻))): ℋ⟶
ℋ |
21 | 2, 19, 20 | pjsdii 30103 |
. . . . . . . . 9
⊢
((projℎ‘𝐻) ∘
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) =
(((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ 𝐻))) +op
((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) |
22 | 12, 2 | pjss1coi 30111 |
. . . . . . . . . . 11
⊢ ((𝐺 ∩ 𝐻) ⊆ 𝐻 ↔
((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ 𝐻))) = (projℎ‘(𝐺 ∩ 𝐻))) |
23 | 6, 22 | mpbi 233 |
. . . . . . . . . 10
⊢
((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ 𝐻))) = (projℎ‘(𝐺 ∩ 𝐻)) |
24 | 2, 14 | pjorthcoi 30117 |
. . . . . . . . . . 11
⊢ (𝐻 ⊆ (⊥‘(𝐺 ∩ (⊥‘𝐻))) →
((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ (⊥‘𝐻)))) = 0hop ) |
25 | 10, 24 | ax-mp 5 |
. . . . . . . . . 10
⊢
((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ (⊥‘𝐻)))) = 0hop |
26 | 23, 25 | oveq12i 7195 |
. . . . . . . . 9
⊢
(((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ 𝐻))) +op
((projℎ‘𝐻) ∘
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) =
((projℎ‘(𝐺 ∩ 𝐻)) +op 0hop
) |
27 | 19 | hoaddid1i 29734 |
. . . . . . . . 9
⊢
((projℎ‘(𝐺 ∩ 𝐻)) +op 0hop ) =
(projℎ‘(𝐺 ∩ 𝐻)) |
28 | 21, 26, 27 | 3eqtri 2766 |
. . . . . . . 8
⊢
((projℎ‘𝐻) ∘
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) =
(projℎ‘(𝐺 ∩ 𝐻)) |
29 | 28 | eqeq2i 2752 |
. . . . . . 7
⊢
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) = ((projℎ‘𝐻) ∘
((projℎ‘(𝐺 ∩ 𝐻)) +op
(projℎ‘(𝐺 ∩ (⊥‘𝐻))))) ↔
((projℎ‘𝐻) ∘
(projℎ‘𝐺)) = (projℎ‘(𝐺 ∩ 𝐻))) |
30 | | coeq2 5711 |
. . . . . . . 8
⊢
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) = (projℎ‘(𝐺 ∩ 𝐻)) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) = ((projℎ‘𝐺) ∘
(projℎ‘(𝐺 ∩ 𝐻)))) |
31 | | inss1 4129 |
. . . . . . . . 9
⊢ (𝐺 ∩ 𝐻) ⊆ 𝐺 |
32 | 12, 1 | pjss1coi 30111 |
. . . . . . . . 9
⊢ ((𝐺 ∩ 𝐻) ⊆ 𝐺 ↔
((projℎ‘𝐺) ∘
(projℎ‘(𝐺 ∩ 𝐻))) = (projℎ‘(𝐺 ∩ 𝐻))) |
33 | 31, 32 | mpbi 233 |
. . . . . . . 8
⊢
((projℎ‘𝐺) ∘
(projℎ‘(𝐺 ∩ 𝐻))) = (projℎ‘(𝐺 ∩ 𝐻)) |
34 | 30, 33 | eqtrdi 2790 |
. . . . . . 7
⊢
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) = (projℎ‘(𝐺 ∩ 𝐻)) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) = (projℎ‘(𝐺 ∩ 𝐻))) |
35 | 29, 34 | sylbi 220 |
. . . . . 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 220 |
. . . 4
⊢
((projℎ‘𝐺) = (projℎ‘((𝐺 ∩ 𝐻) ∨ℋ (𝐺 ∩ (⊥‘𝐻)))) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) = (projℎ‘(𝐺 ∩ 𝐻))) |
38 | 5, 37 | syl 17 |
. . 3
⊢ (𝐺 𝐶ℋ
𝐻 →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) = (projℎ‘(𝐺 ∩ 𝐻))) |
39 | 1, 2 | cmcm3i 29542 |
. . . . 5
⊢ (𝐺 𝐶ℋ
𝐻 ↔
(⊥‘𝐺)
𝐶ℋ 𝐻) |
40 | 7, 2 | cmbri 29538 |
. . . . 5
⊢
((⊥‘𝐺)
𝐶ℋ 𝐻 ↔ (⊥‘𝐺) = (((⊥‘𝐺) ∩ 𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻)))) |
41 | 39, 40 | bitri 278 |
. . . 4
⊢ (𝐺 𝐶ℋ
𝐻 ↔
(⊥‘𝐺) =
(((⊥‘𝐺) ∩
𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻)))) |
42 | | fveq2 6687 |
. . . . 5
⊢
((⊥‘𝐺) =
(((⊥‘𝐺) ∩
𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻))) →
(projℎ‘(⊥‘𝐺)) =
(projℎ‘(((⊥‘𝐺) ∩ 𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻))))) |
43 | | inss2 4130 |
. . . . . . . . 9
⊢
((⊥‘𝐺)
∩ 𝐻) ⊆ 𝐻 |
44 | 2, 1 | chub2i 29418 |
. . . . . . . . . 10
⊢ 𝐻 ⊆ (𝐺 ∨ℋ 𝐻) |
45 | 1, 2 | chdmm4i 29428 |
. . . . . . . . . 10
⊢
(⊥‘((⊥‘𝐺) ∩ (⊥‘𝐻))) = (𝐺 ∨ℋ 𝐻) |
46 | 44, 45 | sseqtrri 3924 |
. . . . . . . . 9
⊢ 𝐻 ⊆
(⊥‘((⊥‘𝐺) ∩ (⊥‘𝐻))) |
47 | 43, 46 | sstri 3896 |
. . . . . . . 8
⊢
((⊥‘𝐺)
∩ 𝐻) ⊆
(⊥‘((⊥‘𝐺) ∩ (⊥‘𝐻))) |
48 | 7, 2 | chincli 29408 |
. . . . . . . . 9
⊢
((⊥‘𝐺)
∩ 𝐻) ∈
Cℋ |
49 | 7, 13 | chincli 29408 |
. . . . . . . . 9
⊢
((⊥‘𝐺)
∩ (⊥‘𝐻))
∈ Cℋ |
50 | 48, 49 | pjscji 30118 |
. . . . . . . 8
⊢
(((⊥‘𝐺)
∩ 𝐻) ⊆
(⊥‘((⊥‘𝐺) ∩ (⊥‘𝐻))) →
(projℎ‘(((⊥‘𝐺) ∩ 𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻)))) =
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) |
51 | 47, 50 | ax-mp 5 |
. . . . . . 7
⊢
(projℎ‘(((⊥‘𝐺) ∩ 𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻)))) =
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻)))) |
52 | 51 | eqeq2i 2752 |
. . . . . 6
⊢
((projℎ‘(⊥‘𝐺)) =
(projℎ‘(((⊥‘𝐺) ∩ 𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻)))) ↔
(projℎ‘(⊥‘𝐺)) =
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) |
53 | | coeq2 5711 |
. . . . . . 7
⊢
((projℎ‘(⊥‘𝐺)) =
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻)))) →
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))) = ((projℎ‘𝐻) ∘
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻)))))) |
54 | 48 | pjfi 29652 |
. . . . . . . . . . 11
⊢
(projℎ‘((⊥‘𝐺) ∩ 𝐻)): ℋ⟶ ℋ |
55 | 49 | pjfi 29652 |
. . . . . . . . . . 11
⊢
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))): ℋ⟶
ℋ |
56 | 2, 54, 55 | pjsdii 30103 |
. . . . . . . . . 10
⊢
((projℎ‘𝐻) ∘
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) =
(((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) +op
((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) |
57 | 48, 2 | pjss1coi 30111 |
. . . . . . . . . . . 12
⊢
(((⊥‘𝐺)
∩ 𝐻) ⊆ 𝐻 ↔
((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) |
58 | 43, 57 | mpbi 233 |
. . . . . . . . . . 11
⊢
((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻)) |
59 | 2, 49 | pjorthcoi 30117 |
. . . . . . . . . . . 12
⊢ (𝐻 ⊆
(⊥‘((⊥‘𝐺) ∩ (⊥‘𝐻))) →
((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻)))) = 0hop ) |
60 | 46, 59 | ax-mp 5 |
. . . . . . . . . . 11
⊢
((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻)))) = 0hop |
61 | 58, 60 | oveq12i 7195 |
. . . . . . . . . 10
⊢
(((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) +op
((projℎ‘𝐻) ∘
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) =
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op 0hop
) |
62 | 54 | hoaddid1i 29734 |
. . . . . . . . . 10
⊢
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op 0hop ) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻)) |
63 | 56, 61, 62 | 3eqtri 2766 |
. . . . . . . . 9
⊢
((projℎ‘𝐻) ∘
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻)) |
64 | 63 | eqeq2i 2752 |
. . . . . . . 8
⊢
(((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))) = ((projℎ‘𝐻) ∘
((projℎ‘((⊥‘𝐺) ∩ 𝐻)) +op
(projℎ‘((⊥‘𝐺) ∩ (⊥‘𝐻))))) ↔
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) |
65 | | coeq2 5711 |
. . . . . . . . 9
⊢
(((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻)) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) = ((projℎ‘𝐺) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻)))) |
66 | 1, 13 | chub1i 29417 |
. . . . . . . . . . 11
⊢ 𝐺 ⊆ (𝐺 ∨ℋ (⊥‘𝐻)) |
67 | 1, 2 | chdmm2i 29426 |
. . . . . . . . . . 11
⊢
(⊥‘((⊥‘𝐺) ∩ 𝐻)) = (𝐺 ∨ℋ (⊥‘𝐻)) |
68 | 66, 67 | sseqtrri 3924 |
. . . . . . . . . 10
⊢ 𝐺 ⊆
(⊥‘((⊥‘𝐺) ∩ 𝐻)) |
69 | 1, 48 | pjorthcoi 30117 |
. . . . . . . . . 10
⊢ (𝐺 ⊆
(⊥‘((⊥‘𝐺) ∩ 𝐻)) →
((projℎ‘𝐺) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) = 0hop ) |
70 | 68, 69 | ax-mp 5 |
. . . . . . . . 9
⊢
((projℎ‘𝐺) ∘
(projℎ‘((⊥‘𝐺) ∩ 𝐻))) = 0hop |
71 | 65, 70 | eqtrdi 2790 |
. . . . . . . 8
⊢
(((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))) =
(projℎ‘((⊥‘𝐺) ∩ 𝐻)) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) = 0hop ) |
72 | 64, 71 | sylbi 220 |
. . . . . . 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 220 |
. . . . 5
⊢
((projℎ‘(⊥‘𝐺)) =
(projℎ‘(((⊥‘𝐺) ∩ 𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻)))) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) = 0hop ) |
75 | 42, 74 | syl 17 |
. . . 4
⊢
((⊥‘𝐺) =
(((⊥‘𝐺) ∩
𝐻) ∨ℋ
((⊥‘𝐺) ∩
(⊥‘𝐻))) →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) = 0hop ) |
76 | 41, 75 | sylbi 220 |
. . 3
⊢ (𝐺 𝐶ℋ
𝐻 →
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) = 0hop ) |
77 | 38, 76 | oveq12d 7201 |
. 2
⊢ (𝐺 𝐶ℋ
𝐻 →
(((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) +op
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))))) =
((projℎ‘(𝐺 ∩ 𝐻)) +op 0hop
)) |
78 | | df-iop 29697 |
. . . . . . 7
⊢
Iop = (projℎ‘ ℋ) |
79 | 78 | coeq2i 5713 |
. . . . . 6
⊢
((projℎ‘𝐻) ∘ Iop ) =
((projℎ‘𝐻) ∘ (projℎ‘
ℋ)) |
80 | 2 | pjfi 29652 |
. . . . . . 7
⊢
(projℎ‘𝐻): ℋ⟶ ℋ |
81 | 80 | hoid1i 29737 |
. . . . . 6
⊢
((projℎ‘𝐻) ∘ Iop ) =
(projℎ‘𝐻) |
82 | 79, 81 | eqtr3i 2764 |
. . . . 5
⊢
((projℎ‘𝐻) ∘ (projℎ‘
ℋ)) = (projℎ‘𝐻) |
83 | 1 | pjtoi 30127 |
. . . . . . 7
⊢
((projℎ‘𝐺) +op
(projℎ‘(⊥‘𝐺))) = (projℎ‘
ℋ) |
84 | 83 | coeq2i 5713 |
. . . . . 6
⊢
((projℎ‘𝐻) ∘
((projℎ‘𝐺) +op
(projℎ‘(⊥‘𝐺)))) = ((projℎ‘𝐻) ∘
(projℎ‘ ℋ)) |
85 | 1 | pjfi 29652 |
. . . . . . 7
⊢
(projℎ‘𝐺): ℋ⟶ ℋ |
86 | 7 | pjfi 29652 |
. . . . . . 7
⊢
(projℎ‘(⊥‘𝐺)): ℋ⟶ ℋ |
87 | 2, 85, 86 | pjsdii 30103 |
. . . . . 6
⊢
((projℎ‘𝐻) ∘
((projℎ‘𝐺) +op
(projℎ‘(⊥‘𝐺)))) =
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) +op
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) |
88 | 84, 87 | eqtr3i 2764 |
. . . . 5
⊢
((projℎ‘𝐻) ∘ (projℎ‘
ℋ)) = (((projℎ‘𝐻) ∘
(projℎ‘𝐺)) +op
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) |
89 | 82, 88 | eqtr3i 2764 |
. . . 4
⊢
(projℎ‘𝐻) = (((projℎ‘𝐻) ∘
(projℎ‘𝐺)) +op
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺)))) |
90 | 89 | coeq2i 5713 |
. . 3
⊢
((projℎ‘𝐺) ∘
(projℎ‘𝐻)) = ((projℎ‘𝐺) ∘
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) +op
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))))) |
91 | 80, 85 | hocofi 29714 |
. . . 4
⊢
((projℎ‘𝐻) ∘
(projℎ‘𝐺)): ℋ⟶ ℋ |
92 | 80, 86 | hocofi 29714 |
. . . 4
⊢
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))): ℋ⟶
ℋ |
93 | 1, 91, 92 | pjsdii 30103 |
. . 3
⊢
((projℎ‘𝐺) ∘
(((projℎ‘𝐻) ∘
(projℎ‘𝐺)) +op
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))))) =
(((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) +op
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))))) |
94 | 90, 93 | eqtr2i 2763 |
. 2
⊢
(((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘𝐺))) +op
((projℎ‘𝐺) ∘
((projℎ‘𝐻) ∘
(projℎ‘(⊥‘𝐺))))) =
((projℎ‘𝐺) ∘
(projℎ‘𝐻)) |
95 | 77, 94, 27 | 3eqtr3g 2797 |
1
⊢ (𝐺 𝐶ℋ
𝐻 →
((projℎ‘𝐺) ∘
(projℎ‘𝐻)) = (projℎ‘(𝐺 ∩ 𝐻))) |