Metamath Proof Explorer

Theorem ltrncom

Description: Composition is commutative for translations. Part of proof of Lemma G of Crawley p. 116. (Contributed by NM, 5-Jun-2013)

Ref Expression
Hypotheses ltrncom.h 
|- H = ( LHyp ` K )
ltrncom.t 
|- T = ( ( LTrn ` K ) ` W )
Assertion ltrncom 
|- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( F o. G ) = ( G o. F ) )

Proof

Step Hyp Ref Expression
1 ltrncom.h 
 |-  H = ( LHyp ` K )
2 ltrncom.t 
 |-  T = ( ( LTrn ` K ) ` W )
3 simpl1 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F = ( _I |` ( Base ` K ) ) ) -> ( K e. HL /\ W e. H ) )
4 simpl2 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F = ( _I |` ( Base ` K ) ) ) -> F e. T )
5 simpl3 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F = ( _I |` ( Base ` K ) ) ) -> G e. T )
6 simpr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F = ( _I |` ( Base ` K ) ) ) -> F = ( _I |` ( Base ` K ) ) )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 7 1 2 cdlemg47a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` ( Base ` K ) ) ) -> ( F o. G ) = ( G o. F ) )
9 3 4 5 6 8 syl121anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F = ( _I |` ( Base ` K ) ) ) -> ( F o. G ) = ( G o. F ) )
10 simpll1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F =/= ( _I |` ( Base ` K ) ) ) /\ ( ( ( trL ` K ) ` W ) ` F ) = ( ( ( trL ` K ) ` W ) ` G ) ) -> ( K e. HL /\ W e. H ) )
11 simpll2 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F =/= ( _I |` ( Base ` K ) ) ) /\ ( ( ( trL ` K ) ` W ) ` F ) = ( ( ( trL ` K ) ` W ) ` G ) ) -> F e. T )
12 simpll3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F =/= ( _I |` ( Base ` K ) ) ) /\ ( ( ( trL ` K ) ` W ) ` F ) = ( ( ( trL ` K ) ` W ) ` G ) ) -> G e. T )
13 simplr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F =/= ( _I |` ( Base ` K ) ) ) /\ ( ( ( trL ` K ) ` W ) ` F ) = ( ( ( trL ` K ) ` W ) ` G ) ) -> F =/= ( _I |` ( Base ` K ) ) )
14 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F =/= ( _I |` ( Base ` K ) ) ) /\ ( ( ( trL ` K ) ` W ) ` F ) = ( ( ( trL ` K ) ` W ) ` G ) ) -> ( ( ( trL ` K ) ` W ) ` F ) = ( ( ( trL ` K ) ` W ) ` G ) )
15 eqid 
 |-  ( ( trL ` K ) ` W ) = ( ( trL ` K ) ` W )
16 7 1 2 15 cdlemg48 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` ( Base ` K ) ) /\ ( ( ( trL ` K ) ` W ) ` F ) = ( ( ( trL ` K ) ` W ) ` G ) ) ) -> ( F o. G ) = ( G o. F ) )
17 10 11 12 13 14 16 syl122anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F =/= ( _I |` ( Base ` K ) ) ) /\ ( ( ( trL ` K ) ` W ) ` F ) = ( ( ( trL ` K ) ` W ) ` G ) ) -> ( F o. G ) = ( G o. F ) )
18 simpll1 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F =/= ( _I |` ( Base ` K ) ) ) /\ ( ( ( trL ` K ) ` W ) ` F ) =/= ( ( ( trL ` K ) ` W ) ` G ) ) -> ( K e. HL /\ W e. H ) )
19 simpll2 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F =/= ( _I |` ( Base ` K ) ) ) /\ ( ( ( trL ` K ) ` W ) ` F ) =/= ( ( ( trL ` K ) ` W ) ` G ) ) -> F e. T )
20 simpll3 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F =/= ( _I |` ( Base ` K ) ) ) /\ ( ( ( trL ` K ) ` W ) ` F ) =/= ( ( ( trL ` K ) ` W ) ` G ) ) -> G e. T )
21 simpr 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F =/= ( _I |` ( Base ` K ) ) ) /\ ( ( ( trL ` K ) ` W ) ` F ) =/= ( ( ( trL ` K ) ` W ) ` G ) ) -> ( ( ( trL ` K ) ` W ) ` F ) =/= ( ( ( trL ` K ) ` W ) ` G ) )
22 1 2 15 cdlemg44 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( ( trL ` K ) ` W ) ` F ) =/= ( ( ( trL ` K ) ` W ) ` G ) ) -> ( F o. G ) = ( G o. F ) )
23 18 19 20 21 22 syl121anc 
 |-  ( ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F =/= ( _I |` ( Base ` K ) ) ) /\ ( ( ( trL ` K ) ` W ) ` F ) =/= ( ( ( trL ` K ) ` W ) ` G ) ) -> ( F o. G ) = ( G o. F ) )
24 17 23 pm2.61dane 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ F =/= ( _I |` ( Base ` K ) ) ) -> ( F o. G ) = ( G o. F ) )
25 9 24 pm2.61dane 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( F o. G ) = ( G o. F ) )