tendo1ne0

Description: The identity (unity) is not equal to the zero trace-preserving endomorphism. (Contributed by NM, 8-Aug-2013)

	Ref	Expression
Hypotheses	tendoid0.b	$⊢ B = {Base}_{K}$
	tendoid0.h	$⊢ H = LHyp (K)$
	tendoid0.t	$⊢ T = LTrn (K) (W)$
	tendoid0.e	$⊢ E = TEndo (K) (W)$
	tendoid0.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
Assertion	tendo1ne0	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \neq O$

Proof

Step	Hyp	Ref	Expression
1		tendoid0.b	$⊢ B = {Base}_{K}$
2		tendoid0.h	$⊢ H = LHyp (K)$
3		tendoid0.t	$⊢ T = LTrn (K) (W)$
4		tendoid0.e	$⊢ E = TEndo (K) (W)$
5		tendoid0.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
6	1 2 3	cdlemftr0	$⊢ (K \in HL \land W \in H) \to \exists g \in T g \neq {I ↾}_{B}$
7		simp3	$⊢ ((K \in HL \land W \in H) \land g \in T \land g \neq {I ↾}_{B}) \to g \neq {I ↾}_{B}$
8		fveq1	$⊢ {I ↾}_{T} = O \to ({I ↾}_{T}) (g) = O (g)$
9	8	adantl	$⊢ (((K \in HL \land W \in H) \land g \in T \land g \neq {I ↾}_{B}) \land {I ↾}_{T} = O) \to ({I ↾}_{T}) (g) = O (g)$
10		simpl2	$⊢ (((K \in HL \land W \in H) \land g \in T \land g \neq {I ↾}_{B}) \land {I ↾}_{T} = O) \to g \in T$
11		fvresi	$⊢ g \in T \to ({I ↾}_{T}) (g) = g$
12	10 11	syl	$⊢ (((K \in HL \land W \in H) \land g \in T \land g \neq {I ↾}_{B}) \land {I ↾}_{T} = O) \to ({I ↾}_{T}) (g) = g$
13	5 1	tendo02	$⊢ g \in T \to O (g) = {I ↾}_{B}$
14	10 13	syl	$⊢ (((K \in HL \land W \in H) \land g \in T \land g \neq {I ↾}_{B}) \land {I ↾}_{T} = O) \to O (g) = {I ↾}_{B}$
15	9 12 14	3eqtr3d	$⊢ (((K \in HL \land W \in H) \land g \in T \land g \neq {I ↾}_{B}) \land {I ↾}_{T} = O) \to g = {I ↾}_{B}$
16	15	ex	$⊢ ((K \in HL \land W \in H) \land g \in T \land g \neq {I ↾}_{B}) \to ({I ↾}_{T} = O \to g = {I ↾}_{B})$
17	16	necon3d	$⊢ ((K \in HL \land W \in H) \land g \in T \land g \neq {I ↾}_{B}) \to (g \neq {I ↾}_{B} \to {I ↾}_{T} \neq O)$
18	7 17	mpd	$⊢ ((K \in HL \land W \in H) \land g \in T \land g \neq {I ↾}_{B}) \to {I ↾}_{T} \neq O$
19	18	rexlimdv3a	$⊢ (K \in HL \land W \in H) \to (\exists g \in T g \neq {I ↾}_{B} \to {I ↾}_{T} \neq O)$
20	6 19	mpd	$⊢ (K \in HL \land W \in H) \to {I ↾}_{T} \neq O$

Metamath Proof Explorer

Theorem tendo1ne0

Proof