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