Metamath Proof Explorer


Theorem ltrncoidN

Description: Two translations are equal if the composition of one with the converse of the other is the zero translation. This is an analogue of vector subtraction. (Contributed by NM, 7-Apr-2014) (New usage is discouraged.)

Ref Expression
Hypotheses ltrn1o.b B = Base K
ltrn1o.h H = LHyp K
ltrn1o.t T = LTrn K W
Assertion ltrncoidN K HL W H F T G T F G -1 = I B F = G

Proof

Step Hyp Ref Expression
1 ltrn1o.b B = Base K
2 ltrn1o.h H = LHyp K
3 ltrn1o.t T = LTrn K W
4 simpl1 K HL W H F T G T F G -1 = I B K HL W H
5 simpl3 K HL W H F T G T F G -1 = I B G T
6 1 2 3 ltrn1o K HL W H G T G : B 1-1 onto B
7 4 5 6 syl2anc K HL W H F T G T F G -1 = I B G : B 1-1 onto B
8 f1ococnv1 G : B 1-1 onto B G -1 G = I B
9 7 8 syl K HL W H F T G T F G -1 = I B G -1 G = I B
10 9 coeq2d K HL W H F T G T F G -1 = I B F G -1 G = F I B
11 simpl2 K HL W H F T G T F G -1 = I B F T
12 1 2 3 ltrn1o K HL W H F T F : B 1-1 onto B
13 4 11 12 syl2anc K HL W H F T G T F G -1 = I B F : B 1-1 onto B
14 f1of F : B 1-1 onto B F : B B
15 fcoi1 F : B B F I B = F
16 13 14 15 3syl K HL W H F T G T F G -1 = I B F I B = F
17 10 16 eqtr2d K HL W H F T G T F G -1 = I B F = F G -1 G
18 coass F G -1 G = F G -1 G
19 17 18 eqtr4di K HL W H F T G T F G -1 = I B F = F G -1 G
20 simpr K HL W H F T G T F G -1 = I B F G -1 = I B
21 20 coeq1d K HL W H F T G T F G -1 = I B F G -1 G = I B G
22 f1of G : B 1-1 onto B G : B B
23 fcoi2 G : B B I B G = G
24 7 22 23 3syl K HL W H F T G T F G -1 = I B I B G = G
25 21 24 eqtrd K HL W H F T G T F G -1 = I B F G -1 G = G
26 19 25 eqtrd K HL W H F T G T F G -1 = I B F = G
27 simpr K HL W H F T G T F = G F = G
28 27 coeq1d K HL W H F T G T F = G F G -1 = G G -1
29 simpl1 K HL W H F T G T F = G K HL W H
30 simpl3 K HL W H F T G T F = G G T
31 29 30 6 syl2anc K HL W H F T G T F = G G : B 1-1 onto B
32 f1ococnv2 G : B 1-1 onto B G G -1 = I B
33 31 32 syl K HL W H F T G T F = G G G -1 = I B
34 28 33 eqtrd K HL W H F T G T F = G F G -1 = I B
35 26 34 impbida K HL W H F T G T F G -1 = I B F = G