Metamath Proof Explorer

Theorem pjadj2coi

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 e. CH
pjadj2co.2 
|- G e. CH
pjadj2co.3 
|- H e. CH
Assertion pjadj2coi 
|- ( ( 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
1 pjadj2co.1 
 |-  F e. CH
2 pjadj2co.2 
 |-  G e. CH
3 pjadj2co.3 
 |-  H e. CH
4 3 pjhcli 
 |-  ( A e. ~H -> ( ( projh ` H ) ` A ) e. ~H )
5 1 2 pjadjcoi 
 |-  ( ( ( ( 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 )
8 3 pjadji 
 |-  ( ( 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 ) )
17 16 adantr 
 |-  ( ( 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 ) ) ) )
24 23 adantl 
 |-  ( ( 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 ) ) ) )
25 10 17 24 3eqtr4d 
 |-  ( ( 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 ) ) )