tendoset

Description: The set of trace-preserving endomorphisms on the set of translations for a fiducial co-atom W . (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	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))\}$

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	tendofset	$⊢ K \in V \to TEndo (K) = (w \in H ⟼ \{s \| (s : LTrn (K) (w) ⟶ LTrn (K) (w) \land \forall f \in LTrn (K) (w) \forall g \in LTrn (K) (w) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (w) trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f))\})$
7	6	fveq1d	$⊢ K \in V \to TEndo (K) (W) = (w \in H ⟼ \{s \| (s : LTrn (K) (w) ⟶ LTrn (K) (w) \land \forall f \in LTrn (K) (w) \forall g \in LTrn (K) (w) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (w) trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f))\}) (W)$
8		fveq2	$⊢ w = W \to LTrn (K) (w) = LTrn (K) (W)$
9	8 8	feq23d	$⊢ w = W \to (s : LTrn (K) (w) ⟶ LTrn (K) (w) \leftrightarrow s : LTrn (K) (W) ⟶ LTrn (K) (W))$
10	8	raleqdv	$⊢ w = W \to (\forall g \in LTrn (K) (w) s (f \circ g) = s (f) \circ s (g) \leftrightarrow \forall g \in LTrn (K) (W) s (f \circ g) = s (f) \circ s (g))$
11	8 10	raleqbidv	$⊢ w = W \to (\forall f \in LTrn (K) (w) \forall g \in LTrn (K) (w) s (f \circ g) = s (f) \circ s (g) \leftrightarrow \forall f \in LTrn (K) (W) \forall g \in LTrn (K) (W) s (f \circ g) = s (f) \circ s (g))$
12		fveq2	$⊢ w = W \to trL (K) (w) = trL (K) (W)$
13	12 4	eqtr4di	$⊢ w = W \to trL (K) (w) = R$
14	13	fveq1d	$⊢ w = W \to trL (K) (w) (s (f)) = R (s (f))$
15	13	fveq1d	$⊢ w = W \to trL (K) (w) (f) = R (f)$
16	14 15	breq12d	$⊢ w = W \to (trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f) \leftrightarrow R (s (f)) \underset{˙}{\leq} R (f))$
17	8 16	raleqbidv	$⊢ w = W \to (\forall f \in LTrn (K) (w) trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f) \leftrightarrow \forall f \in LTrn (K) (W) R (s (f)) \underset{˙}{\leq} R (f))$
18	9 11 17	3anbi123d	$⊢ w = W \to ((s : LTrn (K) (w) ⟶ LTrn (K) (w) \land \forall f \in LTrn (K) (w) \forall g \in LTrn (K) (w) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (w) trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f)) \leftrightarrow (s : LTrn (K) (W) ⟶ LTrn (K) (W) \land \forall f \in LTrn (K) (W) \forall g \in LTrn (K) (W) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (W) R (s (f)) \underset{˙}{\leq} R (f)))$
19	18	abbidv	$⊢ w = W \to \{s \| (s : LTrn (K) (w) ⟶ LTrn (K) (w) \land \forall f \in LTrn (K) (w) \forall g \in LTrn (K) (w) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (w) trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f))\} = \{s \| (s : LTrn (K) (W) ⟶ LTrn (K) (W) \land \forall f \in LTrn (K) (W) \forall g \in LTrn (K) (W) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (W) R (s (f)) \underset{˙}{\leq} R (f))\}$
20		eqid	$⊢ (w \in H ⟼ \{s \| (s : LTrn (K) (w) ⟶ LTrn (K) (w) \land \forall f \in LTrn (K) (w) \forall g \in LTrn (K) (w) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (w) trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f))\}) = (w \in H ⟼ \{s \| (s : LTrn (K) (w) ⟶ LTrn (K) (w) \land \forall f \in LTrn (K) (w) \forall g \in LTrn (K) (w) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (w) trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f))\})$
21		fvex	$⊢ LTrn (K) (W) \in V$
22	21 21	mapval	$⊢ {LTrn (K) (W)}^{LTrn (K) (W)} = \{s \| s : LTrn (K) (W) ⟶ LTrn (K) (W)\}$
23		ovex	$⊢ {LTrn (K) (W)}^{LTrn (K) (W)} \in V$
24	22 23	eqeltrri	$⊢ \{s \| s : LTrn (K) (W) ⟶ LTrn (K) (W)\} \in V$
25		simp1	$⊢ (s : LTrn (K) (W) ⟶ LTrn (K) (W) \land \forall f \in LTrn (K) (W) \forall g \in LTrn (K) (W) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (W) R (s (f)) \underset{˙}{\leq} R (f)) \to s : LTrn (K) (W) ⟶ LTrn (K) (W)$
26	25	ss2abi	$⊢ \{s \| (s : LTrn (K) (W) ⟶ LTrn (K) (W) \land \forall f \in LTrn (K) (W) \forall g \in LTrn (K) (W) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (W) R (s (f)) \underset{˙}{\leq} R (f))\} \subseteq \{s \| s : LTrn (K) (W) ⟶ LTrn (K) (W)\}$
27	24 26	ssexi	$⊢ \{s \| (s : LTrn (K) (W) ⟶ LTrn (K) (W) \land \forall f \in LTrn (K) (W) \forall g \in LTrn (K) (W) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (W) R (s (f)) \underset{˙}{\leq} R (f))\} \in V$
28	19 20 27	fvmpt	$⊢ W \in H \to (w \in H ⟼ \{s \| (s : LTrn (K) (w) ⟶ LTrn (K) (w) \land \forall f \in LTrn (K) (w) \forall g \in LTrn (K) (w) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (w) trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f))\}) (W) = \{s \| (s : LTrn (K) (W) ⟶ LTrn (K) (W) \land \forall f \in LTrn (K) (W) \forall g \in LTrn (K) (W) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (W) R (s (f)) \underset{˙}{\leq} R (f))\}$
29	3 3	feq23i	$⊢ s : T ⟶ T \leftrightarrow s : LTrn (K) (W) ⟶ LTrn (K) (W)$
30	3	raleqi	$⊢ \forall g \in T s (f \circ g) = s (f) \circ s (g) \leftrightarrow \forall g \in LTrn (K) (W) s (f \circ g) = s (f) \circ s (g)$
31	3 30	raleqbii	$⊢ \forall f \in T \forall g \in T s (f \circ g) = s (f) \circ s (g) \leftrightarrow \forall f \in LTrn (K) (W) \forall g \in LTrn (K) (W) s (f \circ g) = s (f) \circ s (g)$
32	3	raleqi	$⊢ \forall f \in T R (s (f)) \underset{˙}{\leq} R (f) \leftrightarrow \forall f \in LTrn (K) (W) R (s (f)) \underset{˙}{\leq} R (f)$
33	29 31 32	3anbi123i	$⊢ (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 : LTrn (K) (W) ⟶ LTrn (K) (W) \land \forall f \in LTrn (K) (W) \forall g \in LTrn (K) (W) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (W) R (s (f)) \underset{˙}{\leq} R (f))$
34	33	abbii	$⊢ \{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))\} = \{s \| (s : LTrn (K) (W) ⟶ LTrn (K) (W) \land \forall f \in LTrn (K) (W) \forall g \in LTrn (K) (W) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (W) R (s (f)) \underset{˙}{\leq} R (f))\}$
35	28 34	eqtr4di	$⊢ W \in H \to (w \in H ⟼ \{s \| (s : LTrn (K) (w) ⟶ LTrn (K) (w) \land \forall f \in LTrn (K) (w) \forall g \in LTrn (K) (w) s (f \circ g) = s (f) \circ s (g) \land \forall f \in LTrn (K) (w) trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f))\}) (W) = \{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))\}$
36	7 35	sylan9eq	$⊢ (K \in V \land W \in H) \to TEndo (K) (W) = \{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))\}$
37	5 36	syl5eq	$⊢ (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))\}$

Metamath Proof Explorer

Theorem tendoset

Proof