This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ↾ 𝐵 ) )