# Metamath Proof Explorer

## 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}}_{ℋ}$
pjclem1.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
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}}_{ℋ}$
2 pjclem1.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 df-iop ${⊢}{I}_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left(ℋ\right)$
4 3 coeq2i ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {I}_{\mathrm{op}}={\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left(ℋ\right)$
5 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ$
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(ℋ\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(ℋ\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)$
10 7 8 9 3eqtr2i ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left(ℋ\right)={\mathrm{proj}}_{ℎ}\left(ℋ\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)$
11 10 oveq1i ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left(ℋ\right)\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(ℋ\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(ℋ\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(ℋ\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(ℋ\right)\right){-}_{\mathrm{op}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(ℋ\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 ${⊢}ℋ\in {\mathbf{C}}_{ℋ}$
15 14 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left(ℋ\right):ℋ⟶ℋ$
16 2 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
17 1 15 16 pjddii ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\circ \left({\mathrm{proj}}_{ℎ}\left(ℋ\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)\right)=\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left(ℋ\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(ℋ\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)=\left({\mathrm{proj}}_{ℎ}\left(ℋ\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(ℋ\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)\right)=\left({\mathrm{proj}}_{ℎ}\left(ℋ\right){-}_{\mathrm{op}}{\mathrm{proj}}_{ℎ}\left({H}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)$
20 2 pjoci ${⊢}{\mathrm{proj}}_{ℎ}\left(ℋ\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(ℋ\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(ℋ\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)$