Metamath Proof Explorer

Theorem tendo0co2

Description: The additive identity trace-preserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 ? (Contributed by NM, 11-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})$
	Assertion	tendo0co2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to O (F \circ G) = O (F) \circ O (G)$

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	2 3	ltrnco	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to F \circ G \in T$
7	5 1	tendo02	$⊢ F \circ G \in T \to O (F \circ G) = {I ↾}_{B}$
8	6 7	syl	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to O (F \circ G) = {I ↾}_{B}$
9	5 1	tendo02	$⊢ F \in T \to O (F) = {I ↾}_{B}$
10	9	3ad2ant2	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to O (F) = {I ↾}_{B}$
11	5 1	tendo02	$⊢ G \in T \to O (G) = {I ↾}_{B}$
12	11	3ad2ant3	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to O (G) = {I ↾}_{B}$
13	10 12	coeq12d	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to O (F) \circ O (G) = ({I ↾}_{B}) \circ ({I ↾}_{B})$
14		f1oi	$⊢ ({I ↾}_{B}) : B \underset{1-1 onto}{⟶} B$
15		f1of	$⊢ ({I ↾}_{B}) : B \underset{1-1 onto}{⟶} B \to ({I ↾}_{B}) : B ⟶ B$
16		fcoi1	$⊢ ({I ↾}_{B}) : B ⟶ B \to ({I ↾}_{B}) \circ ({I ↾}_{B}) = {I ↾}_{B}$
17	14 15 16	mp2b	$⊢ ({I ↾}_{B}) \circ ({I ↾}_{B}) = {I ↾}_{B}$
18	13 17	eqtr2di	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to {I ↾}_{B} = O (F) \circ O (G)$
19	8 18	eqtrd	$⊢ ((K \in HL \land W \in H) \land F \in T \land G \in T) \to O (F \circ G) = O (F) \circ O (G)$