Metamath Proof Explorer


Theorem trlconid

Description: The composition of two different translations is not the identity translation. (Contributed by NM, 22-Jul-2013)

Ref Expression
Hypotheses trlconid.b B = Base K
trlconid.h H = LHyp K
trlconid.t T = LTrn K W
trlconid.r R = trL K W
Assertion trlconid K HL W H F T G T R F R G F G I B

Proof

Step Hyp Ref Expression
1 trlconid.b B = Base K
2 trlconid.h H = LHyp K
3 trlconid.t T = LTrn K W
4 trlconid.r R = trL K W
5 eqid Atoms K = Atoms K
6 5 2 3 4 trlcoat K HL W H F T G T R F R G R F G Atoms K
7 simp1 K HL W H F T G T R F R G K HL W H
8 simp2l K HL W H F T G T R F R G F T
9 simp2r K HL W H F T G T R F R G G T
10 2 3 ltrnco K HL W H F T G T F G T
11 7 8 9 10 syl3anc K HL W H F T G T R F R G F G T
12 1 5 2 3 4 trlnidatb K HL W H F G T F G I B R F G Atoms K
13 7 11 12 syl2anc K HL W H F T G T R F R G F G I B R F G Atoms K
14 6 13 mpbird K HL W H F T G T R F R G F G I B