Metamath Proof Explorer

Theorem pjadjcoi

Description: Adjoint of composition of projections. Special case of Theorem 3.11(viii) of Beran p. 106. (Contributed by NM, 6-Oct-2000) (New usage is discouraged.)

Ref Expression
Hypotheses pjco.1 
|- G e. CH
pjco.2 
|- H e. CH
Assertion pjadjcoi 
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) .ih B ) = ( A .ih ( ( ( projh ` H ) o. ( projh ` G ) ) ` B ) ) )

Proof

Step Hyp Ref Expression
1 pjco.1 
 |-  G e. CH
2 pjco.2 
 |-  H e. CH
3 2 pjhcli 
 |-  ( A e. ~H -> ( ( projh ` H ) ` A ) e. ~H )
4 1 pjadji 
 |-  ( ( ( ( projh ` H ) ` A ) e. ~H /\ B e. ~H ) -> ( ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) .ih B ) = ( ( ( projh ` H ) ` A ) .ih ( ( projh ` G ) ` B ) ) )
5 3 4 sylan 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) .ih B ) = ( ( ( projh ` H ) ` A ) .ih ( ( projh ` G ) ` B ) ) )
6 1 pjhcli 
 |-  ( B e. ~H -> ( ( projh ` G ) ` B ) e. ~H )
7 2 pjadji 
 |-  ( ( A e. ~H /\ ( ( projh ` G ) ` B ) e. ~H ) -> ( ( ( projh ` H ) ` A ) .ih ( ( projh ` G ) ` B ) ) = ( A .ih ( ( projh ` H ) ` ( ( projh ` G ) ` B ) ) ) )
8 6 7 sylan2 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( projh ` H ) ` A ) .ih ( ( projh ` G ) ` B ) ) = ( A .ih ( ( projh ` H ) ` ( ( projh ` G ) ` B ) ) ) )
9 5 8 eqtrd 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) .ih B ) = ( A .ih ( ( projh ` H ) ` ( ( projh ` G ) ` B ) ) ) )
10 1 2 pjcoi 
 |-  ( A e. ~H -> ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) = ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) )
11 10 oveq1d 
 |-  ( A e. ~H -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) .ih B ) = ( ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) .ih B ) )
12 11 adantr 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) .ih B ) = ( ( ( projh ` G ) ` ( ( projh ` H ) ` A ) ) .ih B ) )
13 2 1 pjcoi 
 |-  ( B e. ~H -> ( ( ( projh ` H ) o. ( projh ` G ) ) ` B ) = ( ( projh ` H ) ` ( ( projh ` G ) ` B ) ) )
14 13 oveq2d 
 |-  ( B e. ~H -> ( A .ih ( ( ( projh ` H ) o. ( projh ` G ) ) ` B ) ) = ( A .ih ( ( projh ` H ) ` ( ( projh ` G ) ` B ) ) ) )
15 14 adantl 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( A .ih ( ( ( projh ` H ) o. ( projh ` G ) ) ` B ) ) = ( A .ih ( ( projh ` H ) ` ( ( projh ` G ) ` B ) ) ) )
16 9 12 15 3eqtr4d 
 |-  ( ( A e. ~H /\ B e. ~H ) -> ( ( ( ( projh ` G ) o. ( projh ` H ) ) ` A ) .ih B ) = ( A .ih ( ( ( projh ` H ) o. ( projh ` G ) ) ` B ) ) )