# Metamath Proof Explorer

## Theorem pjcocli

Description: Closure of composition of projections. (Contributed by NM, 29-Nov-2000) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 pjco.1 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
2 pjco.2 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
3 1 2 pjcoi ${⊢}{A}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)$
4 2 pjhcli ${⊢}{A}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in ℋ$
5 1 pjcli ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in ℋ\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\in {G}$
6 4 5 syl ${⊢}{A}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\in {G}$
7 3 6 eqeltrd ${⊢}{A}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\in {G}$