tendo0mulr

Description: Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014)

	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	tendo0mulr	$⊢ ((K \in HL \land W \in H) \land U \in E) \to U \circ O = 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	6	adantr	$⊢ ((K \in HL \land W \in H) \land U \in E) \to \exists g \in T g \neq {I ↾}_{B}$
8		simpll	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to (K \in HL \land W \in H)$
9		simplr	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to U \in E$
10	1 2 3 4 5	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in E$
11	10	ad2antrr	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to O \in E$
12	2 4	tendococl	$⊢ ((K \in HL \land W \in H) \land U \in E \land O \in E) \to U \circ O \in E$
13	8 9 11 12	syl3anc	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to U \circ O \in E$
14	5 1	tendo02	$⊢ g \in T \to O (g) = {I ↾}_{B}$
15	14	ad2antrl	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to O (g) = {I ↾}_{B}$
16	15	fveq2d	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to U (O (g)) = U ({I ↾}_{B})$
17	1 2 4	tendoid	$⊢ ((K \in HL \land W \in H) \land U \in E) \to U ({I ↾}_{B}) = {I ↾}_{B}$
18	17	adantr	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to U ({I ↾}_{B}) = {I ↾}_{B}$
19	16 18	eqtrd	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to U (O (g)) = {I ↾}_{B}$
20		simprl	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to g \in T$
21	2 3 4	tendocoval	$⊢ ((K \in HL \land W \in H) \land (U \in E \land O \in E) \land g \in T) \to (U \circ O) (g) = U (O (g))$
22	8 9 11 20 21	syl121anc	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to (U \circ O) (g) = U (O (g))$
23	19 22 15	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to (U \circ O) (g) = O (g)$
24		simpr	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to (g \in T \land g \neq {I ↾}_{B})$
25	1 2 3 4	tendocan	$⊢ ((K \in HL \land W \in H) \land (U \circ O \in E \land O \in E \land (U \circ O) (g) = O (g)) \land (g \in T \land g \neq {I ↾}_{B})) \to U \circ O = O$
26	8 13 11 23 24 25	syl131anc	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to U \circ O = O$
27	7 26	rexlimddv	$⊢ ((K \in HL \land W \in H) \land U \in E) \to U \circ O = O$

Metamath Proof Explorer

Theorem tendo0mulr

Proof