# Metamath Proof Explorer

## 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}}_{ℋ}$
pjadj2co.2 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
pjadj2co.3 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
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}}_{ℋ}$
2 pjadj2co.2 ${⊢}{G}\in {\mathbf{C}}_{ℋ}$
3 pjadj2co.3 ${⊢}{H}\in {\mathbf{C}}_{ℋ}$
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 ℋ\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 ℋ\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}}_{ℋ}$
9 8 3 chincli ${⊢}\left({F}\cap {G}\right)\cap {H}\in {\mathbf{C}}_{ℋ}$
10 9 pjadji ${⊢}\left({x}\in ℋ\wedge {y}\in ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\wedge {y}\in ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}\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):ℋ⟶ℋ$
26 2 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ$
27 25 26 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right):ℋ⟶ℋ$
28 3 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
29 27 28 hococli ${⊢}{x}\in ℋ\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 ℋ$
30 28 25 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right):ℋ⟶ℋ$
31 30 26 hococli ${⊢}{x}\in ℋ\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 ℋ$
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 ℋ\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 ℋ\right)\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\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}↔\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 ℋ\to \left(\forall {y}\in ℋ\phantom{\rule{.4em}{0ex}}\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}↔\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 ℋ\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 ℋ\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 ℋ\phantom{\rule{.4em}{0ex}}\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):ℋ⟶ℋ$
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):ℋ⟶ℋ$
39 37 38 hoeqi ${⊢}\forall {x}\in ℋ\phantom{\rule{.4em}{0ex}}\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)↔\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)$