trlnid

Description: Different translations with the same trace cannot be the identity. (Contributed by NM, 26-Jul-2013)

	Ref	Expression
Hypotheses	trlnid.b	$⊢ B = {Base}_{K}$
	trlnid.h	$⊢ H = LHyp (K)$
	trlnid.t	$⊢ T = LTrn (K) (W)$
	trlnid.r	$⊢ R = trL (K) (W)$
Assertion	trlnid	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \to F \neq {I ↾}_{B}$

Proof

Step	Hyp	Ref	Expression
1		trlnid.b	$⊢ B = {Base}_{K}$
2		trlnid.h	$⊢ H = LHyp (K)$
3		trlnid.t	$⊢ T = LTrn (K) (W)$
4		trlnid.r	$⊢ R = trL (K) (W)$
5		simp3l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \to F \neq G$
6		simp1	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \to (K \in HL \land W \in H)$
7		simp2l	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \to F \in T$
8		eqid	$⊢ 0. (K) = 0. (K)$
9	1 8 2 3 4	trlid0b	$⊢ ((K \in HL \land W \in H) \land F \in T) \to (F = {I ↾}_{B} \leftrightarrow R (F) = 0. (K))$
10	6 7 9	syl2anc	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \to (F = {I ↾}_{B} \leftrightarrow R (F) = 0. (K))$
11	10	biimpar	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \land R (F) = 0. (K)) \to F = {I ↾}_{B}$
12		simp3r	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \to R (F) = R (G)$
13	12	eqeq1d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \to (R (F) = 0. (K) \leftrightarrow R (G) = 0. (K))$
14	13	biimpa	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \land R (F) = 0. (K)) \to R (G) = 0. (K)$
15		simpl1	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \land R (F) = 0. (K)) \to (K \in HL \land W \in H)$
16		simpl2r	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \land R (F) = 0. (K)) \to G \in T$
17	1 8 2 3 4	trlid0b	$⊢ ((K \in HL \land W \in H) \land G \in T) \to (G = {I ↾}_{B} \leftrightarrow R (G) = 0. (K))$
18	15 16 17	syl2anc	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \land R (F) = 0. (K)) \to (G = {I ↾}_{B} \leftrightarrow R (G) = 0. (K))$
19	14 18	mpbird	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \land R (F) = 0. (K)) \to G = {I ↾}_{B}$
20	11 19	eqtr4d	$⊢ (((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \land R (F) = 0. (K)) \to F = G$
21	20	ex	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \to (R (F) = 0. (K) \to F = G)$
22	10 21	sylbid	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \to (F = {I ↾}_{B} \to F = G)$
23	22	necon3d	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \to (F \neq G \to F \neq {I ↾}_{B})$
24	5 23	mpd	$⊢ ((K \in HL \land W \in H) \land (F \in T \land G \in T) \land (F \neq G \land R (F) = R (G))) \to F \neq {I ↾}_{B}$

Metamath Proof Explorer

Theorem trlnid

Proof