istendo

Description: The predicate "is a trace-preserving endomorphism". Similar to definition of trace-preserving endomorphism in Crawley p. 117, penultimate line. (Contributed by NM, 8-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	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)))$

Proof

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	tendoset	$⊢ (K \in V \land W \in H) \to E = \{s \| (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	6	eleq2d	$⊢ (K \in V \land W \in H) \to (S \in E \leftrightarrow S \in \{s \| (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))\})$
8	3	fvexi	$⊢ T \in V$
9		fex	$⊢ (S : T ⟶ T \land T \in V) \to S \in V$
10	8 9	mpan2	$⊢ S : T ⟶ T \to S \in V$
11	10	3ad2ant1	$⊢ (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 S \in V$
12		feq1	$⊢ s = S \to (s : T ⟶ T \leftrightarrow S : T ⟶ T)$
13		fveq1	$⊢ s = S \to s (f \circ g) = S (f \circ g)$
14		fveq1	$⊢ s = S \to s (f) = S (f)$
15		fveq1	$⊢ s = S \to s (g) = S (g)$
16	14 15	coeq12d	$⊢ s = S \to s (f) \circ s (g) = S (f) \circ S (g)$
17	13 16	eqeq12d	$⊢ s = S \to (s (f \circ g) = s (f) \circ s (g) \leftrightarrow S (f \circ g) = S (f) \circ S (g))$
18	17	2ralbidv	$⊢ s = S \to (\forall f \in T \forall g \in T s (f \circ g) = s (f) \circ s (g) \leftrightarrow \forall f \in T \forall g \in T S (f \circ g) = S (f) \circ S (g))$
19	14	fveq2d	$⊢ s = S \to R (s (f)) = R (S (f))$
20	19	breq1d	$⊢ s = S \to (R (s (f)) \underset{˙}{\leq} R (f) \leftrightarrow R (S (f)) \underset{˙}{\leq} R (f))$
21	20	ralbidv	$⊢ s = S \to (\forall f \in T R (s (f)) \underset{˙}{\leq} R (f) \leftrightarrow \forall f \in T R (S (f)) \underset{˙}{\leq} R (f))$
22	12 18 21	3anbi123d	$⊢ s = S \to ((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)) \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)))$
23	11 22	elab3	$⊢ S \in \{s \| (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))\} \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))$
24	7 23	bitrdi	$⊢ (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)))$

Metamath Proof Explorer

Theorem istendo

Proof