tendofset

Description: The set of all trace-preserving endomorphisms on the set of translations for a lattice K . (Contributed by NM, 8-Jun-2013)

	Ref	Expression
Hypotheses	tendoset.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	tendoset.h	$⊢ H = LHyp (K)$
Assertion	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))\})$

Proof

Step	Hyp	Ref	Expression
1		tendoset.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		tendoset.h	$⊢ H = LHyp (K)$
3		elex	$⊢ K \in V \to K \in V$
4		fveq2	$⊢ k = K \to LHyp (k) = LHyp (K)$
5	4 2	eqtr4di	$⊢ k = K \to LHyp (k) = H$
6		fveq2	$⊢ k = K \to LTrn (k) = LTrn (K)$
7	6	fveq1d	$⊢ k = K \to LTrn (k) (w) = LTrn (K) (w)$
8	7 7	feq23d	$⊢ k = K \to (s : LTrn (k) (w) ⟶ LTrn (k) (w) \leftrightarrow s : LTrn (K) (w) ⟶ LTrn (K) (w))$
9	7	raleqdv	$⊢ k = K \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))$
10	7 9	raleqbidv	$⊢ k = K \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))$
11		fveq2	$⊢ k = K \to trL (k) = trL (K)$
12	11	fveq1d	$⊢ k = K \to trL (k) (w) = trL (K) (w)$
13	12	fveq1d	$⊢ k = K \to trL (k) (w) (s (f)) = trL (K) (w) (s (f))$
14		fveq2	$⊢ k = K \to \leq_{k} = \leq_{K}$
15	14 1	eqtr4di	$⊢ k = K \to \leq_{k} = \underset{˙}{\leq}$
16	12	fveq1d	$⊢ k = K \to trL (k) (w) (f) = trL (K) (w) (f)$
17	13 15 16	breq123d	$⊢ k = K \to (trL (k) (w) (s (f)) \leq_{k} trL (k) (w) (f) \leftrightarrow trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f))$
18	7 17	raleqbidv	$⊢ k = K \to (\forall f \in LTrn (k) (w) trL (k) (w) (s (f)) \leq_{k} trL (k) (w) (f) \leftrightarrow \forall f \in LTrn (K) (w) trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f))$
19	8 10 18	3anbi123d	$⊢ k = K \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)) \leq_{k} 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) trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f)))$
20	19	abbidv	$⊢ k = K \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)) \leq_{k} 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) trL (K) (w) (s (f)) \underset{˙}{\leq} trL (K) (w) (f))\}$
21	5 20	mpteq12dv	$⊢ k = K \to (w \in LHyp (k) ⟼ \{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)) \leq_{k} 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))\})$
22		df-tendo	$⊢ TEndo = (k \in V ⟼ (w \in LHyp (k) ⟼ \{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)) \leq_{k} trL (k) (w) (f))\}))$
23	21 22 2	mptfvmpt	$⊢ 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))\})$
24	3 23	syl	$⊢ 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))\})$

Metamath Proof Explorer

Theorem tendofset

Proof