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}}_{\mathscr{H}}$$
	pjclem1.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pjclem1	$$⊢G{𝐶}_{\mathscr{H}}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}}_{\mathscr{H}}$$
2		pjclem1.2	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
3	1 2	cmbri	$$⊢G{𝐶}_{\mathscr{H}}H\leftrightarrow G=\left(G\cap H\right){\vee }_{\mathscr{H}}\left(G\cap \perp \left(H\right)\right)$$
4		fveq2	$$⊢G=\left(G\cap H\right){\vee }_{\mathscr{H}}\left(G\cap \perp \left(H\right)\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(\left(G\cap H\right){\vee }_{\mathscr{H}}\left(G\cap \perp \left(H\right)\right)\right)$$
5	3 4	sylbi	$$⊢G{𝐶}_{\mathscr{H}}H\to {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(\left(G\cap H\right){\vee }_{\mathscr{H}}\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}}_{\mathscr{H}}$$
8	2 7	chub2i	$$⊢H\subseteq \perp \left(G\right){\vee }_{\mathscr{H}}H$$
9	1 2	chdmm3i	$$⊢\perp \left(G\cap \perp \left(H\right)\right)=\perp \left(G\right){\vee }_{\mathscr{H}}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}}_{\mathscr{H}}$$
13	2	choccli	$$⊢\perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
14	1 13	chincli	$$⊢G\cap \perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
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 }_{\mathscr{H}}\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 }_{\mathscr{H}}\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 }_{\mathscr{H}}\left(G\cap \perp \left(H\right)\right)\right)\leftrightarrow {\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):\mathscr{H}⟶\mathscr{H}$$
20	14	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\cap \perp \left(H\right)\right):\mathscr{H}⟶\mathscr{H}$$
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\leftrightarrow {\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)\leftrightarrow {\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\leftrightarrow {\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	eqtrdi	$$⊢{\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 }_{\mathscr{H}}\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{𝐶}_{\mathscr{H}}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{𝐶}_{\mathscr{H}}H\leftrightarrow \perp \left(G\right){𝐶}_{\mathscr{H}}H$$
40	7 2	cmbri	$$⊢\perp \left(G\right){𝐶}_{\mathscr{H}}H\leftrightarrow \perp \left(G\right)=\left(\perp \left(G\right)\cap H\right){\vee }_{\mathscr{H}}\left(\perp \left(G\right)\cap \perp \left(H\right)\right)$$
41	39 40	bitri	$$⊢G{𝐶}_{\mathscr{H}}H\leftrightarrow \perp \left(G\right)=\left(\perp \left(G\right)\cap H\right){\vee }_{\mathscr{H}}\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 }_{\mathscr{H}}\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 }_{\mathscr{H}}\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 }_{\mathscr{H}}H$$
45	1 2	chdmm4i	$$⊢\perp \left(\perp \left(G\right)\cap \perp \left(H\right)\right)=G{\vee }_{\mathscr{H}}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}}_{\mathscr{H}}$$
49	7 13	chincli	$$⊢\perp \left(G\right)\cap \perp \left(H\right)\in {\mathbf{C}}_{\mathscr{H}}$$
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 }_{\mathscr{H}}\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 }_{\mathscr{H}}\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 }_{\mathscr{H}}\left(\perp \left(G\right)\cap \perp \left(H\right)\right)\right)\leftrightarrow {\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):\mathscr{H}⟶\mathscr{H}$$
55	49	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\cap \perp \left(H\right)\right):\mathscr{H}⟶\mathscr{H}$$
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\leftrightarrow {\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)\leftrightarrow {\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 }_{\mathscr{H}}\perp \left(H\right)$$
67	1 2	chdmm2i	$$⊢\perp \left(\perp \left(G\right)\cap H\right)=G{\vee }_{\mathscr{H}}\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	eqtrdi	$$⊢{\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 }_{\mathscr{H}}\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 }_{\mathscr{H}}\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{𝐶}_{\mathscr{H}}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{𝐶}_{\mathscr{H}}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(\mathscr{H}\right)$$
79	78	coeq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\circ I_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
80	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
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(\mathscr{H}\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(\mathscr{H}\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(\mathscr{H}\right)$$
85	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
86	7	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right):\mathscr{H}⟶\mathscr{H}$$
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(\mathscr{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)$$
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):\mathscr{H}⟶\mathscr{H}$$
92	80 86	hocofi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(G\right)\right)\right):\mathscr{H}⟶\mathscr{H}$$
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{𝐶}_{\mathscr{H}}H\to {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(G\cap H\right)$$