Theorem zlmvsca

Description: Scalar multiplication operation of a ZZ -module. (Contributed by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	zlmbas.w	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
	zlmvsca.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
Assertion	zlmvsca	$$⊢\underset{\dot{}}{·}={\cdot }_W$$

Proof

Step	Hyp	Ref	Expression
1		zlmbas.w	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
2		zlmvsca.2	$$⊢\underset{\dot{}}{·}={\cdot }_G$$
3		ovex	$$⊢G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\in \mathrm{V}$$
4	2	fvexi	$$⊢\underset{\dot{}}{·}\in \mathrm{V}$$
5		vscaid	$$⊢{\cdot }_{𝑠}=\mathrm{Slot}{\cdot }_{\mathrm{ndx}}$$
6	5	setsid	$$⊢\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\in \mathrm{V}\wedge \underset{\dot{}}{·}\in \mathrm{V}\right)\to \underset{\dot{}}{·}={\cdot }_{\left(\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right)}$$
7	3 4 6	mp2an	$$⊢\underset{\dot{}}{·}={\cdot }_{\left(\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right)}$$
8	1 2	zlmval	$$⊢G\in \mathrm{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{}}{·}⟩$$
9	8	fveq2d	$$⊢G\in \mathrm{V}\to {\cdot }_W={\cdot }_{\left(\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},\underset{\dot{}}{·}⟩\right)}$$
10	7 9	eqtr4id	$$⊢G\in \mathrm{V}\to \underset{\dot{}}{·}={\cdot }_W$$
11	5	str0	$$⊢\varnothing ={\cdot }_{\varnothing }$$
12		fvprc	$$⊢\neg G\in \mathrm{V}\to {\cdot }_G=\varnothing$$
13	2 12	syl5eq	$$⊢\neg G\in \mathrm{V}\to \underset{\dot{}}{·}=\varnothing$$
14		fvprc	$$⊢\neg G\in \mathrm{V}\to \mathrm{\mathbb{Z}Mod}\left(G\right)=\varnothing$$
15	1 14	syl5eq	$$⊢\neg G\in \mathrm{V}\to W=\varnothing$$
16	15	fveq2d	$$⊢\neg G\in \mathrm{V}\to {\cdot }_W={\cdot }_{\varnothing }$$
17	11 13 16	3eqtr4a	$$⊢\neg G\in \mathrm{V}\to \underset{\dot{}}{·}={\cdot }_W$$
18	10 17	pm2.61i	$$⊢\underset{\dot{}}{·}={\cdot }_W$$