# Metamath Proof Explorer

## Theorem pjclem2

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

Ref Expression
Hypotheses pjclem1.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjclem1.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
Assertion pjclem2 ${⊢}{G}{𝐶}_{ℋ}{H}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({H}\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 incom ${⊢}{G}\cap {H}={H}\cap {G}$
4 3 fveq2i ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap {G}\right)$
5 1 2 pjclem1 ${⊢}{G}{𝐶}_{ℋ}{H}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({G}\cap {H}\right)$
6 1 2 cmcmi ${⊢}{G}{𝐶}_{ℋ}{H}↔{H}{𝐶}_{ℋ}{G}$
7 2 1 pjclem1 ${⊢}{H}{𝐶}_{ℋ}{G}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap {G}\right)$
8 6 7 sylbi ${⊢}{G}{𝐶}_{ℋ}{H}\to {\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)={\mathrm{proj}}_{ℎ}\left({H}\cap {G}\right)$
9 4 5 8 3eqtr4a ${⊢}{G}{𝐶}_{ℋ}{H}\to {\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)$