# Metamath Proof Explorer

Description: Adjoint of double composition of projections. Generalization of special case of Theorem 3.11(viii) of Beran p. 106. (Contributed by NM, 1-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 pjadj2coi ${⊢}\left({A}\in ℋ\wedge {B}\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({A}\right){\cdot }_{\mathrm{ih}}{B}={A}{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\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 3 pjhcli ${⊢}{A}\in ℋ\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in ℋ$
5 1 2 pjadjcoi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\in ℋ\wedge {B}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{B}={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)$
6 4 5 sylan ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{B}={\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)$
7 2 1 pjcohcli ${⊢}{B}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)\in ℋ$
8 3 pjadji ${⊢}\left({A}\in ℋ\wedge \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)={A}{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)\right)$
9 7 8 sylan2 ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right){\cdot }_{\mathrm{ih}}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)={A}{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)\right)$
10 6 9 eqtrd ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to \left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{B}={A}{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)\right)$
11 1 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({F}\right):ℋ⟶ℋ$
12 2 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({G}\right):ℋ⟶ℋ$
13 11 12 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right):ℋ⟶ℋ$
14 3 pjfi ${⊢}{\mathrm{proj}}_{ℎ}\left({H}\right):ℋ⟶ℋ$
15 13 14 hocoi ${⊢}{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)=\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right)$
16 15 oveq1d ${⊢}{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){\cdot }_{\mathrm{ih}}{B}=\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{B}$
17 16 adantr ${⊢}\left({A}\in ℋ\wedge {B}\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({A}\right){\cdot }_{\mathrm{ih}}{B}=\left({\mathrm{proj}}_{ℎ}\left({F}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\left({\mathrm{proj}}_{ℎ}\left({H}\right)\left({A}\right)\right){\cdot }_{\mathrm{ih}}{B}$
18 coass ${⊢}\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)$
19 18 fveq1i ${⊢}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)=\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\right)\left({B}\right)$
20 12 11 hocofi ${⊢}\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right):ℋ⟶ℋ$
21 14 20 hocoi ${⊢}{B}\in ℋ\to \left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ \left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\right)\left({B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)\right)$
22 19 21 syl5eq ${⊢}{B}\in ℋ\to \left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)={\mathrm{proj}}_{ℎ}\left({H}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)\right)$
23 22 oveq2d ${⊢}{B}\in ℋ\to {A}{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)={A}{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)\right)$
24 23 adantl ${⊢}\left({A}\in ℋ\wedge {B}\in ℋ\right)\to {A}{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)={A}{\cdot }_{\mathrm{ih}}{\mathrm{proj}}_{ℎ}\left({H}\right)\left(\left({\mathrm{proj}}_{ℎ}\left({G}\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)\right)$
25 10 17 24 3eqtr4d ${⊢}\left({A}\in ℋ\wedge {B}\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({A}\right){\cdot }_{\mathrm{ih}}{B}={A}{\cdot }_{\mathrm{ih}}\left(\left({\mathrm{proj}}_{ℎ}\left({H}\right)\circ {\mathrm{proj}}_{ℎ}\left({G}\right)\right)\circ {\mathrm{proj}}_{ℎ}\left({F}\right)\right)\left({B}\right)$