# 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
`|- F e. CH`
`|- G e. CH`
`|- H e. CH`
`|- ( ( A e. ~H /\ B e. ~H ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` A ) .ih B ) = ( A .ih ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` B ) ) )`

### Proof

Step Hyp Ref Expression
` |-  F e. CH`
` |-  G e. CH`
` |-  H e. CH`
4 3 pjhcli
` |-  ( A e. ~H -> ( ( projh ` H ) ` A ) e. ~H )`
` |-  ( ( ( ( projh ` H ) ` A ) e. ~H /\ B e. ~H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) ` ( ( projh ` H ) ` A ) ) .ih B ) = ( ( ( projh ` H ) ` A ) .ih ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) ) )`
6 4 5 sylan
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) ` ( ( projh ` H ) ` A ) ) .ih B ) = ( ( ( projh ` H ) ` A ) .ih ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) ) )`
7 2 1 pjcohcli
` |-  ( B e. ~H -> ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) e. ~H )`
` |-  ( ( A e. ~H /\ ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) e. ~H ) -> ( ( ( projh ` H ) ` A ) .ih ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) ) = ( A .ih ( ( projh ` H ) ` ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) ) ) )`
9 7 8 sylan2
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( projh ` H ) ` A ) .ih ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) ) = ( A .ih ( ( projh ` H ) ` ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) ) ) )`
10 6 9 eqtrd
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) ` ( ( projh ` H ) ` A ) ) .ih B ) = ( A .ih ( ( projh ` H ) ` ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) ) ) )`
11 1 pjfi
` |-  ( projh ` F ) : ~H --> ~H`
12 2 pjfi
` |-  ( projh ` G ) : ~H --> ~H`
13 11 12 hocofi
` |-  ( ( projh ` F ) o. ( projh ` G ) ) : ~H --> ~H`
14 3 pjfi
` |-  ( projh ` H ) : ~H --> ~H`
15 13 14 hocoi
` |-  ( A e. ~H -> ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` A ) = ( ( ( projh ` F ) o. ( projh ` G ) ) ` ( ( projh ` H ) ` A ) ) )`
16 15 oveq1d
` |-  ( A e. ~H -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` A ) .ih B ) = ( ( ( ( projh ` F ) o. ( projh ` G ) ) ` ( ( projh ` H ) ` A ) ) .ih B ) )`
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` A ) .ih B ) = ( ( ( ( projh ` F ) o. ( projh ` G ) ) ` ( ( projh ` H ) ` A ) ) .ih B ) )`
18 coass
` |-  ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) = ( ( projh ` H ) o. ( ( projh ` G ) o. ( projh ` F ) ) )`
19 18 fveq1i
` |-  ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` B ) = ( ( ( projh ` H ) o. ( ( projh ` G ) o. ( projh ` F ) ) ) ` B )`
20 12 11 hocofi
` |-  ( ( projh ` G ) o. ( projh ` F ) ) : ~H --> ~H`
21 14 20 hocoi
` |-  ( B e. ~H -> ( ( ( projh ` H ) o. ( ( projh ` G ) o. ( projh ` F ) ) ) ` B ) = ( ( projh ` H ) ` ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) ) )`
22 19 21 syl5eq
` |-  ( B e. ~H -> ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` B ) = ( ( projh ` H ) ` ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) ) )`
23 22 oveq2d
` |-  ( B e. ~H -> ( A .ih ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` B ) ) = ( A .ih ( ( projh ` H ) ` ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) ) ) )`
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` B ) ) = ( A .ih ( ( projh ` H ) ` ( ( ( projh ` G ) o. ( projh ` F ) ) ` B ) ) ) )`
` |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( ( ( projh ` F ) o. ( projh ` G ) ) o. ( projh ` H ) ) ` A ) .ih B ) = ( A .ih ( ( ( ( projh ` H ) o. ( projh ` G ) ) o. ( projh ` F ) ) ` B ) ) )`