tendoid0

Description: A trace-preserving endomorphism is the additive identity iff at least one of its values (at a non-identity translation) is the identity translation. (Contributed by NM, 1-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	tendoid0	$⊢ ((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \to (U (F) = {I ↾}_{B} \leftrightarrow U = 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		simp3l	$⊢ ((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \to F \in T$
7	5 1	tendo02	$⊢ F \in T \to O (F) = {I ↾}_{B}$
8	6 7	syl	$⊢ ((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \to O (F) = {I ↾}_{B}$
9	8	eqeq2d	$⊢ ((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \to (U (F) = O (F) \leftrightarrow U (F) = {I ↾}_{B})$
10		simpl1	$⊢ (((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \land U (F) = O (F)) \to (K \in HL \land W \in H)$
11		simpl2	$⊢ (((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \land U (F) = O (F)) \to U \in E$
12	1 2 3 4 5	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in E$
13	10 12	syl	$⊢ (((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \land U (F) = O (F)) \to O \in E$
14		simpr	$⊢ (((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \land U (F) = O (F)) \to U (F) = O (F)$
15		simpl3l	$⊢ (((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \land U (F) = O (F)) \to F \in T$
16		simpl3r	$⊢ (((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \land U (F) = O (F)) \to F \neq {I ↾}_{B}$
17	1 2 3 4	tendocan	$⊢ ((K \in HL \land W \in H) \land (U \in E \land O \in E \land U (F) = O (F)) \land (F \in T \land F \neq {I ↾}_{B})) \to U = O$
18	10 11 13 14 15 16 17	syl132anc	$⊢ (((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \land U (F) = O (F)) \to U = O$
19	18	ex	$⊢ ((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \to (U (F) = O (F) \to U = O)$
20	9 19	sylbird	$⊢ ((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \to (U (F) = {I ↾}_{B} \to U = O)$
21		fveq1	$⊢ U = O \to U (F) = O (F)$
22	21	eqeq1d	$⊢ U = O \to (U (F) = {I ↾}_{B} \leftrightarrow O (F) = {I ↾}_{B})$
23	8 22	syl5ibrcom	$⊢ ((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \to (U = O \to U (F) = {I ↾}_{B})$
24	20 23	impbid	$⊢ ((K \in HL \land W \in H) \land U \in E \land (F \in T \land F \neq {I ↾}_{B})) \to (U (F) = {I ↾}_{B} \leftrightarrow U = O)$

Metamath Proof Explorer

Theorem tendoid0

Proof