tendo0mul

Description: Additive identity multiplied by a trace-preserving endomorphism. (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	tendo0mul	$⊢ ((K \in HL \land W \in H) \land U \in E) \to O \circ 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	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	1 2 3 4 5	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in E$
10	9	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$
11		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$
12	2 4	tendococl	$⊢ ((K \in HL \land W \in H) \land O \in E \land U \in E) \to O \circ U \in E$
13	8 10 11 12	syl3anc	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to O \circ U \in E$
14		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$
15	2 3 4	tendocl	$⊢ ((K \in HL \land W \in H) \land U \in E \land g \in T) \to U (g) \in T$
16	8 11 14 15	syl3anc	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to U (g) \in T$
17	5 1	tendo02	$⊢ U (g) \in T \to O (U (g)) = {I ↾}_{B}$
18	16 17	syl	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to O (U (g)) = {I ↾}_{B}$
19	2 3 4	tendocoval	$⊢ ((K \in HL \land W \in H) \land (O \in E \land U \in E) \land g \in T) \to (O \circ U) (g) = O (U (g))$
20	8 10 11 14 19	syl121anc	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to (O \circ U) (g) = O (U (g))$
21	5 1	tendo02	$⊢ g \in T \to O (g) = {I ↾}_{B}$
22	21	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}$
23	18 20 22	3eqtr4d	$⊢ (((K \in HL \land W \in H) \land U \in E) \land (g \in T \land g \neq {I ↾}_{B})) \to (O \circ U) (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 (O \circ U \in E \land O \in E \land (O \circ U) (g) = O (g)) \land (g \in T \land g \neq {I ↾}_{B})) \to O \circ U = O$
26	8 13 10 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 O \circ U = O$
27	7 26	rexlimddv	$⊢ ((K \in HL \land W \in H) \land U \in E) \to O \circ U = O$

Metamath Proof Explorer

Theorem tendo0mul

Proof