This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tgrpfset

Description: The translation group maps for a lattice K . (Contributed by NM, 5-Jun-2013)

		Ref	Expression
	Hypothesis	tgrpset.h	$⊢ H = LHyp (K)$
	Assertion	tgrpfset	$⊢ K \in V \to TGrp (K) = (w \in H ⟼ \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩\})$

Proof

Step	Hyp	Ref	Expression
1		tgrpset.h	$⊢ H = LHyp (K)$
2		elex	$⊢ K \in V \to K \in V$
3		fveq2	$⊢ k = K \to LHyp (k) = LHyp (K)$
4	3 1	eqtr4di	$⊢ k = K \to LHyp (k) = H$
5		fveq2	$⊢ k = K \to LTrn (k) = LTrn (K)$
6	5	fveq1d	$⊢ k = K \to LTrn (k) (w) = LTrn (K) (w)$
7	6	opeq2d	$⊢ k = K \to ⟨{Base}_{ndx}, LTrn (k) (w)⟩ = ⟨{Base}_{ndx}, LTrn (K) (w)⟩$
8		eqidd	$⊢ k = K \to f \circ g = f \circ g$
9	6 6 8	mpoeq123dv	$⊢ k = K \to (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g) = (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)$
10	9	opeq2d	$⊢ k = K \to ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩ = ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩$
11	7 10	preq12d	$⊢ k = K \to \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩\} = \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩\}$
12	4 11	mpteq12dv	$⊢ k = K \to (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩\}) = (w \in H ⟼ \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩\})$
13		df-tgrp	$⊢ TGrp = (k \in V ⟼ (w \in LHyp (k) ⟼ \{⟨{Base}_{ndx}, LTrn (k) (w)⟩, ⟨+_{ndx}, (f \in LTrn (k) (w), g \in LTrn (k) (w) ⟼ f \circ g)⟩\}))$
14	12 13 1	mptfvmpt	$⊢ K \in V \to TGrp (K) = (w \in H ⟼ \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩\})$
15	2 14	syl	$⊢ K \in V \to TGrp (K) = (w \in H ⟼ \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩\})$