Theorem pjclem3

Description: Lemma for projection commutation theorem. (Contributed by NM, 26-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	pjclem3	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\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		df-iop	$$⊢I_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
4	3	coeq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ I_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)$$
5	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
6	5	hoid1i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ I_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(G\right)$$
7	4 6	eqtr3i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)={\mathrm{proj}}_{ℎ}\left(G\right)$$
8	5	hoid1ri	$$⊢I_{\mathrm{op}}\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(G\right)$$
9	3	coeq1i	$$⊢I_{\mathrm{op}}\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$
10	7 8 9	3eqtr2i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)={\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$
11	10	oveq1i	$$⊢\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
12		oveq2	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to \left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)$$
13	11 12	syl5eq	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to \left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)$$
14		helch	$$⊢\mathscr{H}\in {\mathbf{C}}_{\mathscr{H}}$$
15	14	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right):\mathscr{H}⟶\mathscr{H}$$
16	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
17	1 15 16	pjddii	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ \left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)$$
18	15 16 5	hocsubdiri	$$⊢\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)=\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)$$
19	13 17 18	3eqtr4g	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\circ \left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$
20	2	pjoci	$$⊢{\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)$$
21	20	coeq2i	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ \left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)$$
22	20	coeq1i	$$⊢\left({\mathrm{proj}}_{ℎ}\left(\mathscr{H}\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left(H\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$
23	19 21 22	3eqtr3g	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\to {\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)={\mathrm{proj}}_{ℎ}\left(\perp \left(H\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$