Theorem zlmsca

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

	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		5re	$$⊢5\in ℝ$$
4		5lt6	$$⊢5<6$$
5	3 4	ltneii	$$⊢5\ne 6$$
6		scandx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$$
7		vscandx	$$⊢{\cdot }_{\mathrm{ndx}}=6$$
8	6 7	neeq12i	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\leftrightarrow 5\ne 6$$
9	5 8	mpbir	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
10	2 9	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)$$
11		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
12	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)$$
13	11 12	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)$$
14		eqid	$$⊢{\cdot }_G={\cdot }_G$$
15	1 14	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⟩$$
16	15	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)$$
17	10 13 16	3eqtr4a	$$⊢G\in V\to {\mathbb{Z}}_{\mathrm{ring}}=\mathrm{Scalar}\left(W\right)$$