# Metamath Proof Explorer

## Theorem pj2cocli

Description: Closure of double composition of projections. (Contributed by NM, 2-Dec-2000) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 pjadj2co.1 ${⊢}{F}\in {\mathbf{C}}_{ℋ}$
2 pjadj2co.2 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
3 pjadj2co.3 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
4 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({F}\right):ℋ⟶ℋ$
5 2 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ$
6 3 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
7 4 5 6 ho2coi ${⊢}{A}\in ℋ\to \left(\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)={\mathrm{proj}}_{ℎ}\left({F}\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\right)$
8 3 pjhcli ${⊢}{A}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in ℋ$
9 2 pjhcli ${⊢}{\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 ℋ$
10 1 pjcli ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\in ℋ\to {\mathrm{proj}}_{ℎ}\left({F}\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\right)\in {F}$
11 8 9 10 3syl ${⊢}{A}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({F}\right)\left({\mathrm{proj}}_{ℎ}\left({G}\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)\right)\in {F}$
12 7 11 eqeltrd ${⊢}{A}\in ℋ\to \left(\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({H}\right)\right)\left({A}\right)\in {F}$