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 𝐵 = ( Base ‘ 𝐾 )
ltrn1o.h 𝐻 = ( LHyp ‘ 𝐾 )
ltrn1o.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
Assertion ltrncnvnid ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ltrn1o.b 𝐵 = ( Base ‘ 𝐾 )
2 ltrn1o.h 𝐻 = ( LHyp ‘ 𝐾 )
3 ltrn1o.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4 simp3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )
5 1 2 3 ltrn1o ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇 ) → 𝐹 : 𝐵1-1-onto𝐵 )
6 5 3adant3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝐹 : 𝐵1-1-onto𝐵 )
7 f1orel ( 𝐹 : 𝐵1-1-onto𝐵 → Rel 𝐹 )
8 6 7 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → Rel 𝐹 )
9 dfrel2 ( Rel 𝐹 𝐹 = 𝐹 )
10 8 9 sylib ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝐹 = 𝐹 )
11 cnveq ( 𝐹 = ( I ↾ 𝐵 ) → 𝐹 = ( I ↾ 𝐵 ) )
12 10 11 sylan9req ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → 𝐹 = ( I ↾ 𝐵 ) )
13 cnvresid ( I ↾ 𝐵 ) = ( I ↾ 𝐵 )
14 12 13 eqtrdi ( ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) ∧ 𝐹 = ( I ↾ 𝐵 ) ) → 𝐹 = ( I ↾ 𝐵 ) )
15 14 ex ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝐹 = ( I ↾ 𝐵 ) → 𝐹 = ( I ↾ 𝐵 ) ) )
16 15 necon3d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → ( 𝐹 ≠ ( I ↾ 𝐵 ) → 𝐹 ≠ ( I ↾ 𝐵 ) ) )
17 4 16 mpd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝐹𝑇𝐹 ≠ ( I ↾ 𝐵 ) ) → 𝐹 ≠ ( I ↾ 𝐵 ) )