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}}_{\mathscr{H}}$$
	pjadj2co.2	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
	pjadj2co.3	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	pj2cocli	$$⊢A\in \mathscr{H}\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}}_{\mathscr{H}}$$
2		pjadj2co.2	$$⊢G\in {\mathbf{C}}_{\mathscr{H}}$$
3		pjadj2co.3	$$⊢H\in {\mathbf{C}}_{\mathscr{H}}$$
4	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(F\right):\mathscr{H}⟶\mathscr{H}$$
5	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
6	3	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
7	4 5 6	ho2coi	$$⊢A\in \mathscr{H}\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 \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}$$
9	2	pjhcli	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\in \mathscr{H}\to {\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\in \mathscr{H}$$
10	1	pjcli	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right)\left({\mathrm{proj}}_{ℎ}\left(H\right)\left(A\right)\right)\in \mathscr{H}\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 \mathscr{H}\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 \mathscr{H}\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$$