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 HL W H F T G T R F R G R F G 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 HL W H F T G T F G T
6 5 3expb K HL W H F T G T F G T
7 eqid Base K = Base K
8 eqid 0. K = 0. K
9 7 8 2 3 4 trlid0b K HL W H F G T F G = I Base K R F G = 0. K
10 6 9 syldan K HL W H F T G T F G = I Base K R F G = 0. K
11 coass F -1 F G = F -1 F G
12 simpll K HL W H F T G T F G = I Base K K HL W H
13 simplrl K HL W H F T G T F G = I Base K F T
14 7 2 3 ltrn1o K HL W H F T F : Base K 1-1 onto Base K
15 12 13 14 syl2anc K HL W H F T G T F G = I Base K F : Base K 1-1 onto Base K
16 f1ococnv1 F : Base K 1-1 onto Base K F -1 F = I Base K
17 15 16 syl K HL W H F T G T F G = I Base K F -1 F = I Base K
18 17 coeq1d K HL W H F T G T F G = I Base K F -1 F G = I Base K G
19 coeq2 F G = I Base K F -1 F G = F -1 I Base K
20 19 adantl K HL W H F T G T F G = I Base K F -1 F G = F -1 I Base K
21 11 18 20 3eqtr3a K HL W H F T G T F G = I Base K I Base K G = F -1 I Base K
22 simplrr K HL W H F T G T F G = I Base K G T
23 7 2 3 ltrn1o K HL W H G T G : Base K 1-1 onto Base K
24 12 22 23 syl2anc K HL W H F T G T F 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 G = G
27 24 25 26 3syl K HL W H F T G T F G = I Base K I Base K G = G
28 2 3 ltrncnv K HL W H F T F -1 T
29 12 13 28 syl2anc K HL W H F T G T F G = I Base K F -1 T
30 7 2 3 ltrn1o K HL W H F -1 T F -1 : Base K 1-1 onto Base K
31 12 29 30 syl2anc K HL W H F T G T F G = I Base K F -1 : Base K 1-1 onto Base K
32 f1of F -1 : Base K 1-1 onto Base K F -1 : Base K Base K
33 fcoi1 F -1 : Base K Base K F -1 I Base K = F -1
34 31 32 33 3syl K HL W H F T G T F G = I Base K F -1 I Base K = F -1
35 21 27 34 3eqtr3d K HL W H F T G T F G = I Base K G = F -1
36 35 fveq2d K HL W H F T G T F G = I Base K R G = R F -1
37 2 3 4 trlcnv K HL W H F T R F -1 = R F
38 12 13 37 syl2anc K HL W H F T G T F G = I Base K R F -1 = R F
39 36 38 eqtr2d K HL W H F T G T F G = I Base K R F = R G
40 39 ex K HL W H F T G T F G = I Base K R F = R G
41 10 40 sylbird K HL W H F T G T R F G = 0. K R F = R G
42 41 necon3d K HL W H F T G T R F R G R F G 0. K
43 8 1 2 3 4 trlatn0 K HL W H F G T R F G A R F G 0. K
44 6 43 syldan K HL W H F T G T R F G A R F G 0. K
45 42 44 sylibrd K HL W H F T G T R F R G R F G A
46 45 3impia K HL W H F T G T R F R G R F G A