# Metamath Proof Explorer

## Theorem pjclem1

Description: Lemma for projection commutation theorem. (Contributed by NM, 16-Nov-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjclem1.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjclem1.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pjclem1 ${⊢}{G}{𝐶}_{ℋ}{H}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right)$

### Proof

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