tgrpset

Description: The translation group for a fiducial co-atom W . (Contributed by NM, 5-Jun-2013)

	Ref	Expression
Hypotheses	tgrpset.h	$⊢ H = LHyp (K)$
	tgrpset.t	$⊢ T = LTrn (K) (W)$
	tgrpset.g	$⊢ G = TGrp (K) (W)$
Assertion	tgrpset	$⊢ (K \in V \land W \in H) \to G = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩\}$

Proof

Step	Hyp	Ref	Expression
1		tgrpset.h	$⊢ H = LHyp (K)$
2		tgrpset.t	$⊢ T = LTrn (K) (W)$
3		tgrpset.g	$⊢ G = TGrp (K) (W)$
4	1	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)⟩\})$
5	4	fveq1d	$⊢ K \in V \to TGrp (K) (W) = (w \in H ⟼ \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩\}) (W)$
6		fveq2	$⊢ w = W \to LTrn (K) (w) = LTrn (K) (W)$
7	6	opeq2d	$⊢ w = W \to ⟨{Base}_{ndx}, LTrn (K) (w)⟩ = ⟨{Base}_{ndx}, LTrn (K) (W)⟩$
8		eqidd	$⊢ w = W \to f \circ g = f \circ g$
9	6 6 8	mpoeq123dv	$⊢ w = W \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	$⊢ w = W \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	$⊢ w = W \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		eqid	$⊢ (w \in H ⟼ \{⟨{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		prex	$⊢ \{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\} \in V$
14	11 12 13	fvmpt	$⊢ W \in H \to (w \in H ⟼ \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩\}) (W) = \{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\}$
15	2	opeq2i	$⊢ ⟨{Base}_{ndx}, T⟩ = ⟨{Base}_{ndx}, LTrn (K) (W)⟩$
16		eqid	$⊢ f \circ g = f \circ g$
17	2 2 16	mpoeq123i	$⊢ (f \in T, g \in T ⟼ f \circ g) = (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)$
18	17	opeq2i	$⊢ ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩ = ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩$
19	15 18	preq12i	$⊢ \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩\} = \{⟨{Base}_{ndx}, LTrn (K) (W)⟩, ⟨+_{ndx}, (f \in LTrn (K) (W), g \in LTrn (K) (W) ⟼ f \circ g)⟩\}$
20	14 19	eqtr4di	$⊢ W \in H \to (w \in H ⟼ \{⟨{Base}_{ndx}, LTrn (K) (w)⟩, ⟨+_{ndx}, (f \in LTrn (K) (w), g \in LTrn (K) (w) ⟼ f \circ g)⟩\}) (W) = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩\}$
21	5 20	sylan9eq	$⊢ (K \in V \land W \in H) \to TGrp (K) (W) = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩\}$
22	3 21	syl5eq	$⊢ (K \in V \land W \in H) \to G = \{⟨{Base}_{ndx}, T⟩, ⟨+_{ndx}, (f \in T, g \in T ⟼ f \circ g)⟩\}$

Metamath Proof Explorer

Theorem tgrpset

Proof