tendo0pl

Description: Property of the additive identity endormorphism. (Contributed by NM, 12-Jun-2013)

	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	tendo0pl	$⊢ ((K \in HL \land W \in H) \land S \in E) \to O P S = S$

Proof

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		simpl	$⊢ ((K \in HL \land W \in H) \land S \in E) \to (K \in HL \land W \in H)$
8	1 2 3 4 5	tendo0cl	$⊢ (K \in HL \land W \in H) \to O \in E$
9	8	adantr	$⊢ ((K \in HL \land W \in H) \land S \in E) \to O \in E$
10		simpr	$⊢ ((K \in HL \land W \in H) \land S \in E) \to S \in E$
11	2 3 4 6	tendoplcl	$⊢ ((K \in HL \land W \in H) \land O \in E \land S \in E) \to O P S \in E$
12	7 9 10 11	syl3anc	$⊢ ((K \in HL \land W \in H) \land S \in E) \to O P S \in E$
13		simpll	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to (K \in HL \land W \in H)$
14	13 8	syl	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to O \in E$
15		simplr	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to S \in E$
16		simpr	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to g \in T$
17	6 3	tendopl2	$⊢ (O \in E \land S \in E \land g \in T) \to (O P S) (g) = O (g) \circ S (g)$
18	14 15 16 17	syl3anc	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to (O P S) (g) = O (g) \circ S (g)$
19	5 1	tendo02	$⊢ g \in T \to O (g) = {I ↾}_{B}$
20	19	adantl	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to O (g) = {I ↾}_{B}$
21	20	coeq1d	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to O (g) \circ S (g) = ({I ↾}_{B}) \circ S (g)$
22	2 3 4	tendocl	$⊢ ((K \in HL \land W \in H) \land S \in E \land g \in T) \to S (g) \in T$
23	22	3expa	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to S (g) \in T$
24	1 2 3	ltrn1o	$⊢ ((K \in HL \land W \in H) \land S (g) \in T) \to S (g) : B \underset{1-1 onto}{⟶} B$
25	13 23 24	syl2anc	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to S (g) : B \underset{1-1 onto}{⟶} B$
26		f1of	$⊢ S (g) : B \underset{1-1 onto}{⟶} B \to S (g) : B ⟶ B$
27		fcoi2	$⊢ S (g) : B ⟶ B \to ({I ↾}_{B}) \circ S (g) = S (g)$
28	25 26 27	3syl	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to ({I ↾}_{B}) \circ S (g) = S (g)$
29	18 21 28	3eqtrd	$⊢ (((K \in HL \land W \in H) \land S \in E) \land g \in T) \to (O P S) (g) = S (g)$
30	29	ralrimiva	$⊢ ((K \in HL \land W \in H) \land S \in E) \to \forall g \in T (O P S) (g) = S (g)$
31	2 3 4	tendoeq1	$⊢ ((K \in HL \land W \in H) \land (O P S \in E \land S \in E) \land \forall g \in T (O P S) (g) = S (g)) \to O P S = S$
32	7 12 10 30 31	syl121anc	$⊢ ((K \in HL \land W \in H) \land S \in E) \to O P S = S$

Metamath Proof Explorer

Theorem tendo0pl

Proof