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