Theorem zlmsca

Description: Scalar ring of a ZZ -module. (Contributed by Mario Carneiro, 2-Oct-2015) (Revised by AV, 12-Jun-2019) (Proof shortened by AV, 2-Nov-2024)

	Ref	Expression
Hypothesis	zlmbas.w	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
Assertion	zlmsca	$$⊢G\in V\to {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(W\right)$$

Proof

Step	Hyp	Ref	Expression
1		zlmbas.w	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
2		scaid	$$⊢\mathrm{Scalar}=\mathrm{Slot}\mathrm{Scalar}\left(\mathrm{ndx}\right)$$
3		vscandxnscandx	$$⊢{\cdot }_{\mathrm{ndx}}\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
4	3	necomi	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
5	2 4	setsnid	$$⊢\mathrm{Scalar}\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)=\mathrm{Scalar}\left(\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_G⟩\right)$$
6		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
7	2	setsid	$$⊢\left(G\in V\wedge {\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\right)\to {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)$$
8	6 7	mpan2	$$⊢G\in V\to {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)$$
9		eqid	$$⊢{\cdot }_G={\cdot }_G$$
10	1 9	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}},{\cdot }_G⟩$$
11	10	fveq2d	$$⊢G\in V\to \mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_G⟩\right)$$
12	5 8 11	3eqtr4a	$$⊢G\in V\to {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(W\right)$$