Metamath Proof Explorer

Theorem trlcoat

Description: The trace of a composition of two translations is an atom if their traces are different. (Contributed by NM, 15-Jun-2013)

Ref Expression
Hypotheses trlcoat.a 
|- A = ( Atoms ` K )
trlcoat.h 
|- H = ( LHyp ` K )
trlcoat.t 
|- T = ( ( LTrn ` K ) ` W )
trlcoat.r 
|- R = ( ( trL ` K ) ` W )
Assertion trlcoat 
|- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( R ` ( F o. G ) ) e. A )

Proof

Step Hyp Ref Expression
1 trlcoat.a 
 |-  A = ( Atoms ` K )
2 trlcoat.h 
 |-  H = ( LHyp ` K )
3 trlcoat.t 
 |-  T = ( ( LTrn ` K ) ` W )
4 trlcoat.r 
 |-  R = ( ( trL ` K ) ` W )
5 2 3 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( F o. G ) e. T )
6 5 3expb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) -> ( F o. G ) e. T )
7 eqid 
 |-  ( Base ` K ) = ( Base ` K )
8 eqid 
 |-  ( 0. ` K ) = ( 0. ` K )
9 7 8 2 3 4 trlid0b 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F o. G ) e. T ) -> ( ( F o. G ) = ( _I |` ( Base ` K ) ) <-> ( R ` ( F o. G ) ) = ( 0. ` K ) ) )
10 6 9 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) -> ( ( F o. G ) = ( _I |` ( Base ` K ) ) <-> ( R ` ( F o. G ) ) = ( 0. ` K ) ) )
11 coass 
 |-  ( ( `' F o. F ) o. G ) = ( `' F o. ( F o. G ) )
12 simpll 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> ( K e. HL /\ W e. H ) )
13 simplrl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> F e. T )
14 7 2 3 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
15 12 13 14 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
16 f1ococnv1 
 |-  ( F : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> ( `' F o. F ) = ( _I |` ( Base ` K ) ) )
17 15 16 syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> ( `' F o. F ) = ( _I |` ( Base ` K ) ) )
18 17 coeq1d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> ( ( `' F o. F ) o. G ) = ( ( _I |` ( Base ` K ) ) o. G ) )
19 coeq2 
 |-  ( ( F o. G ) = ( _I |` ( Base ` K ) ) -> ( `' F o. ( F o. G ) ) = ( `' F o. ( _I |` ( Base ` K ) ) ) )
20 19 adantl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> ( `' F o. ( F o. G ) ) = ( `' F o. ( _I |` ( Base ` K ) ) ) )
21 11 18 20 3eqtr3a 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> ( ( _I |` ( Base ` K ) ) o. G ) = ( `' F o. ( _I |` ( Base ` K ) ) ) )
22 simplrr 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> G e. T )
23 7 2 3 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ G e. T ) -> G : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
24 12 22 23 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> G : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
25 f1of 
 |-  ( G : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> G : ( Base ` K ) --> ( Base ` K ) )
26 fcoi2 
 |-  ( G : ( Base ` K ) --> ( Base ` K ) -> ( ( _I |` ( Base ` K ) ) o. G ) = G )
27 24 25 26 3syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> ( ( _I |` ( Base ` K ) ) o. G ) = G )
28 2 3 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> `' F e. T )
29 12 13 28 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> `' F e. T )
30 7 2 3 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ `' F e. T ) -> `' F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
31 12 29 30 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> `' F : ( Base ` K ) -1-1-onto-> ( Base ` K ) )
32 f1of 
 |-  ( `' F : ( Base ` K ) -1-1-onto-> ( Base ` K ) -> `' F : ( Base ` K ) --> ( Base ` K ) )
33 fcoi1 
 |-  ( `' F : ( Base ` K ) --> ( Base ` K ) -> ( `' F o. ( _I |` ( Base ` K ) ) ) = `' F )
34 31 32 33 3syl 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> ( `' F o. ( _I |` ( Base ` K ) ) ) = `' F )
35 21 27 34 3eqtr3d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> G = `' F )
36 35 fveq2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> ( R ` G ) = ( R ` `' F ) )
37 2 3 4 trlcnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` `' F ) = ( R ` F ) )
38 12 13 37 syl2anc 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> ( R ` `' F ) = ( R ` F ) )
39 36 38 eqtr2d 
 |-  ( ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) /\ ( F o. G ) = ( _I |` ( Base ` K ) ) ) -> ( R ` F ) = ( R ` G ) )
40 39 ex 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) -> ( ( F o. G ) = ( _I |` ( Base ` K ) ) -> ( R ` F ) = ( R ` G ) ) )
41 10 40 sylbird 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) -> ( ( R ` ( F o. G ) ) = ( 0. ` K ) -> ( R ` F ) = ( R ` G ) ) )
42 41 necon3d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) -> ( ( R ` F ) =/= ( R ` G ) -> ( R ` ( F o. G ) ) =/= ( 0. ` K ) ) )
43 8 1 2 3 4 trlatn0 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F o. G ) e. T ) -> ( ( R ` ( F o. G ) ) e. A <-> ( R ` ( F o. G ) ) =/= ( 0. ` K ) ) )
44 6 43 syldan 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) -> ( ( R ` ( F o. G ) ) e. A <-> ( R ` ( F o. G ) ) =/= ( 0. ` K ) ) )
45 42 44 sylibrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) ) -> ( ( R ` F ) =/= ( R ` G ) -> ( R ` ( F o. G ) ) e. A ) )
46 45 3impia 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( R ` ( F o. G ) ) e. A )