Theorem zlmval

Description: Augment an abelian group with vector space operations to turn it into a ZZ -module. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 12-Jun-2019)

	Ref	Expression
Hypotheses	zlmval.w	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
	zlmval.m	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	zlmval	$$⊢G\in V\to W=\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$

Proof

Step	Hyp	Ref	Expression
1		zlmval.w	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
2		zlmval.m	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		elex	$$⊢G\in V\to G\in \mathrm{V}$$
4		oveq1	$$⊢g=G\to g\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩=G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩$$
5		fveq2	$$⊢g=G\to {\cdot }_g={\cdot }_G$$
6	5 2	eqtr4di	$$⊢g=G\to {\cdot }_g=\underset{\dot{}}{·}$$
7	6	opeq2d	$$⊢g=G\to ⟨{\cdot }_{\mathrm{ndx}},{\cdot }_g⟩=⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$
8	4 7	oveq12d	$$⊢g=G\to \left(g\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_g⟩=\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$
9		df-zlm	$$⊢\mathrm{\mathbb{Z}Mod}=\left(g\in \mathrm{V}⟼\left(g\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_g⟩\right)$$
10		ovex	$$⊢\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\in \mathrm{V}$$
11	8 9 10	fvmpt	$$⊢G\in \mathrm{V}\to \mathrm{\mathbb{Z}Mod}\left(G\right)=\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$
12	3 11	syl	$$⊢G\in V\to \mathrm{\mathbb{Z}Mod}\left(G\right)=\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$
13	1 12	syl5eq	$$⊢G\in V\to W=\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩$$