tendof

Description: Functionality of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013)

	Ref	Expression
Hypotheses	tendof.h	$⊢ H = LHyp (K)$
	tendof.t	$⊢ T = LTrn (K) (W)$
	tendof.e	$⊢ E = TEndo (K) (W)$
Assertion	tendof	$⊢ ((K \in V \land W \in H) \land S \in E) \to S : T ⟶ T$

Step	Hyp	Ref	Expression
1		tendof.h	$⊢ H = LHyp (K)$
2		tendof.t	$⊢ T = LTrn (K) (W)$
3		tendof.e	$⊢ E = TEndo (K) (W)$
4		eqid	$⊢ \leq_{K} = \leq_{K}$
5		eqid	$⊢ trL (K) (W) = trL (K) (W)$
6	4 1 2 5 3	istendo	$⊢ (K \in V \land W \in H) \to (S \in E \leftrightarrow (S : T ⟶ T \land \forall f \in T \forall g \in T S (f \circ g) = S (f) \circ S (g) \land \forall f \in T trL (K) (W) (S (f)) \leq_{K} trL (K) (W) (f)))$
7		simp1	$⊢ (S : T ⟶ T \land \forall f \in T \forall g \in T S (f \circ g) = S (f) \circ S (g) \land \forall f \in T trL (K) (W) (S (f)) \leq_{K} trL (K) (W) (f)) \to S : T ⟶ T$
8	6 7	syl6bi	$⊢ (K \in V \land W \in H) \to (S \in E \to S : T ⟶ T)$
9	8	imp	$⊢ ((K \in V \land W \in H) \land S \in E) \to S : T ⟶ T$

Metamath Proof Explorer