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 \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to F^{-1} \neq {I ↾}_{B}$

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 \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to F \neq {I ↾}_{B}$
5	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land F \in T) \to F : B \underset{1-1 onto}{⟶} B$
6	5	3adant3	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to F : B \underset{1-1 onto}{⟶} B$
7		f1orel	$⊢ F : B \underset{1-1 onto}{⟶} B \to Rel F$
8	6 7	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to Rel F$
9		dfrel2	$⊢ Rel F \leftrightarrow {F^{-1}}^{-1} = F$
10	8 9	sylib	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to {F^{-1}}^{-1} = F$
11		cnveq	$⊢ F^{-1} = {I ↾}_{B} \to {F^{-1}}^{-1} = {({I ↾}_{B})}^{-1}$
12	10 11	sylan9req	$⊢ (((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \land F^{-1} = {I ↾}_{B}) \to F = {({I ↾}_{B})}^{-1}$
13		cnvresid	$⊢ {({I ↾}_{B})}^{-1} = {I ↾}_{B}$
14	12 13	eqtrdi	$⊢ (((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \land F^{-1} = {I ↾}_{B}) \to F = {I ↾}_{B}$
15	14	ex	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to (F^{-1} = {I ↾}_{B} \to F = {I ↾}_{B})$
16	15	necon3d	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to (F \neq {I ↾}_{B} \to F^{-1} \neq {I ↾}_{B})$
17	4 16	mpd	$⊢ ((K \in HL \land W \in H) \land F \in T \land F \neq {I ↾}_{B}) \to F^{-1} \neq {I ↾}_{B}$

Metamath Proof Explorer