tendo0plr

Description: Property of the additive identity endormorphism. (Contributed by NM, 21-Feb-2014)

	Ref	Expression
Hypotheses	tendo0.b	$⊢ B = {Base}_{K}$
	tendo0.h	$⊢ H = LHyp (K)$
	tendo0.t	$⊢ T = LTrn (K) (W)$
	tendo0.e	$⊢ E = TEndo (K) (W)$
	tendo0.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
	tendo0pl.p	$⊢ P = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
Assertion	tendo0plr	$⊢ ((K \in HL \land W \in H) \land S \in E) \to S P O = S$

Step	Hyp	Ref	Expression
1		tendo0.b	$⊢ B = {Base}_{K}$
2		tendo0.h	$⊢ H = LHyp (K)$
3		tendo0.t	$⊢ T = LTrn (K) (W)$
4		tendo0.e	$⊢ E = TEndo (K) (W)$
5		tendo0.o	$⊢ O = (f \in T ⟼ {I ↾}_{B})$
6		tendo0pl.p	$⊢ P = (s \in E, t \in E ⟼ (f \in T ⟼ s (f) \circ t (f)))$
7	1 2 3 4 5	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in E$
8	7	adantr	$⊢ ((K \in HL \land W \in H) \land S \in E) \to O \in E$
9	2 3 4 6	tendoplcom	$⊢ ((K \in HL \land W \in H) \land S \in E \land O \in E) \to S P O = O P S$
10	8 9	mpd3an3	$⊢ ((K \in HL \land W \in H) \land S \in E) \to S P O = O P S$
11	1 2 3 4 5 6	tendo0pl	$⊢ ((K \in HL \land W \in H) \land S \in E) \to O P S = S$
12	10 11	eqtrd	$⊢ ((K \in HL \land W \in H) \land S \in E) \to S P O = S$

Metamath Proof Explorer