tendotp

Description: Trace-preserving property of 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)$
Assertion	tendotp	$⊢ ((K \in V \land W \in H) \land S \in E \land F \in T) \to R (S (F)) \underset{˙}{\leq} R (F)$

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	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)))$
7		2fveq3	$⊢ f = F \to R (S (f)) = R (S (F))$
8		fveq2	$⊢ f = F \to R (f) = R (F)$
9	7 8	breq12d	$⊢ f = F \to (R (S (f)) \underset{˙}{\leq} R (f) \leftrightarrow R (S (F)) \underset{˙}{\leq} R (F))$
10	9	rspccv	$⊢ \forall f \in T R (S (f)) \underset{˙}{\leq} R (f) \to (F \in T \to R (S (F)) \underset{˙}{\leq} R (F))$
11	10	3ad2ant3	$⊢ (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)) \to (F \in T \to R (S (F)) \underset{˙}{\leq} R (F))$
12	6 11	syl6bi	$⊢ (K \in V \land W \in H) \to (S \in E \to (F \in T \to R (S (F)) \underset{˙}{\leq} R (F)))$
13	12	3imp	$⊢ ((K \in V \land W \in H) \land S \in E \land F \in T) \to R (S (F)) \underset{˙}{\leq} R (F)$

Metamath Proof Explorer