istendod

Description: Deduce the predicate "is a trace-preserving endomorphism". (Contributed by NM, 9-Jun-2013)

	Ref	Expression
Hypotheses	tendoset.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	tendoset.h	$⊢ H = LHyp (K)$
	tendoset.t	$⊢ T = LTrn (K) (W)$
	tendoset.r	$⊢ R = trL (K) (W)$
	tendoset.e	$⊢ E = TEndo (K) (W)$
	istendod.1	$⊢ φ \to (K \in V \land W \in H)$
	istendod.2	$⊢ φ \to S : T ⟶ T$
	istendod.3	$⊢ (φ \land f \in T \land g \in T) \to S (f \circ g) = S (f) \circ S (g)$
	istendod.4	$⊢ (φ \land f \in T) \to R (S (f)) \underset{˙}{\leq} R (f)$
Assertion	istendod	$⊢ φ \to S \in E$

Step	Hyp	Ref	Expression
1		tendoset.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		tendoset.h	$⊢ H = LHyp (K)$
3		tendoset.t	$⊢ T = LTrn (K) (W)$
4		tendoset.r	$⊢ R = trL (K) (W)$
5		tendoset.e	$⊢ E = TEndo (K) (W)$
6		istendod.1	$⊢ φ \to (K \in V \land W \in H)$
7		istendod.2	$⊢ φ \to S : T ⟶ T$
8		istendod.3	$⊢ (φ \land f \in T \land g \in T) \to S (f \circ g) = S (f) \circ S (g)$
9		istendod.4	$⊢ (φ \land f \in T) \to R (S (f)) \underset{˙}{\leq} R (f)$
10	8	3expb	$⊢ (φ \land (f \in T \land g \in T)) \to S (f \circ g) = S (f) \circ S (g)$
11	10	ralrimivva	$⊢ φ \to \forall f \in T \forall g \in T S (f \circ g) = S (f) \circ S (g)$
12	9	ralrimiva	$⊢ φ \to \forall f \in T R (S (f)) \underset{˙}{\leq} R (f)$
13	1 2 3 4 5	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 R (S (f)) \underset{˙}{\leq} R (f)))$
14	6 13	syl	$⊢ φ \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 R (S (f)) \underset{˙}{\leq} R (f)))$
15	7 11 12 14	mpbir3and	$⊢ φ \to S \in E$

Metamath Proof Explorer