Theorem pj3cor1i

Description: Projection triplet corollary. (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	pj3cor1i	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$

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		fveq1	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)$$
5	4	oveq2d	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\to x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)=x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)$$
6	5	adantl	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)=x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)$$
7	6	ad2antlr	$$⊢\left(\left(x\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)=x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)$$
8	1 2	chincli	$$⊢F\cap G\in {\mathbf{C}}_{\mathscr{H}}$$
9	8 3	chincli	$$⊢\left(F\cap G\right)\cap H\in {\mathbf{C}}_{\mathscr{H}}$$
10	9	pjadji	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(y\right)$$
11	10	adantlr	$$⊢\left(\left(x\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\wedge y\in \mathscr{H}\right)\to {\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(y\right)$$
12	1 2 3	pj3i	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)$$
13	12	fveq1d	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(x\right)$$
14	13	oveq1d	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(x\right){\cdot }_{\mathrm{ih}}y$$
15	14	ad2antlr	$$⊢\left(\left(x\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\wedge y\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(x\right){\cdot }_{\mathrm{ih}}y$$
16	12	fveq1d	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)={\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(y\right)$$
17	16	oveq2d	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)=x{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(y\right)$$
18	17	ad2antlr	$$⊢\left(\left(x\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\wedge y\in \mathscr{H}\right)\to x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)=x{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left(\left(F\cap G\right)\cap H\right)\left(y\right)$$
19	11 15 18	3eqtr4d	$$⊢\left(\left(x\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\wedge y\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)$$
20	3 1 2	pjadj2coi	$$⊢\left(x\in \mathscr{H}\wedge y\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)$$
21	20	adantlr	$$⊢\left(\left(x\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\wedge y\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=x{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(y\right)$$
22	7 19 21	3eqtr4d	$$⊢\left(\left(x\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\right)\wedge y\in \mathscr{H}\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y$$
23	22	exp31	$$⊢x\in \mathscr{H}\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left(y\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(x\right){\cdot }_{\mathrm{ih}}y=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)\right)$$
24	23	ralrimdv	$$⊢x\in \mathscr{H}\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \forall y\in \mathscr{H}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\right)$$
25	1	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(F\right):\mathscr{H}⟶\mathscr{H}$$
26	2	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(G\right):\mathscr{H}⟶\mathscr{H}$$
27	25 26	hocofi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right):\mathscr{H}⟶\mathscr{H}$$
28	3	pjfi	$$⊢{\mathrm{proj}}_{ℎ}\left(H\right):\mathscr{H}⟶\mathscr{H}$$
29	27 28	hococli	$$⊢x\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(x\right)\in \mathscr{H}$$
30	28 25	hocofi	$$⊢\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right):\mathscr{H}⟶\mathscr{H}$$
31	30 26	hococli	$$⊢x\in \mathscr{H}\to \left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)\in \mathscr{H}$$
32		hial2eq	$$⊢\left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)\in \mathscr{H}\wedge \left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)\in \mathscr{H}\right)\to \left(\forall y\in \mathscr{H}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\leftrightarrow \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)\right)$$
33	29 31 32	syl2anc	$$⊢x\in \mathscr{H}\to \left(\forall y\in \mathscr{H}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right){\cdot }_{\mathrm{ih}}y\leftrightarrow \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)\right)$$
34	24 33	sylibd	$$⊢x\in \mathscr{H}\to \left(\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)\right)$$
35	34	com12	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left(x\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(x\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)\right)$$
36	35	ralrimiv	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \forall x\in \mathscr{H}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)$$
37	27 28	hocofi	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right):\mathscr{H}⟶\mathscr{H}$$
38	30 26	hocofi	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right):\mathscr{H}⟶\mathscr{H}$$
39	37 38	hoeqi	$$⊢\forall x\in \mathscr{H}\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\left(x\right)=\left(\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\left(x\right)\leftrightarrow \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$
40	36 39	sylib	$$⊢\left(\left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\wedge \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(G\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)\right)\to \left({\mathrm{proj}}_{ℎ}\left(F\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(H\right)=\left({\mathrm{proj}}_{ℎ}\left(H\right)\circ {\mathrm{proj}}_{ℎ}\left(F\right)\right)\circ {\mathrm{proj}}_{ℎ}\left(G\right)$$