Metamath Proof Explorer


Theorem ltrncnvnid

Description: If a translation is different from the identity, so is its converse. (Contributed by NM, 17-Jun-2013)

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

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 simp3 K HL W H F T F I B F I B
5 1 2 3 ltrn1o K HL W H F T F : B 1-1 onto B
6 5 3adant3 K HL W H F T F I B F : B 1-1 onto B
7 f1orel F : B 1-1 onto B Rel F
8 6 7 syl K HL W H F T F I B Rel F
9 dfrel2 Rel F F -1 -1 = F
10 8 9 sylib K HL W H F T F I B F -1 -1 = F
11 cnveq F -1 = I B F -1 -1 = I B -1
12 10 11 sylan9req K HL W H F T F I B F -1 = I B F = I B -1
13 cnvresid I B -1 = I B
14 12 13 eqtrdi K HL W H F T F I B F -1 = I B F = I B
15 14 ex K HL W H F T F I B F -1 = I B F = I B
16 15 necon3d K HL W H F T F I B F I B F -1 I B
17 4 16 mpd K HL W H F T F I B F -1 I B