Theorem zlmtset

Description: Topology in a ZZ -module (if present). (Contributed by Thierry Arnoux, 8-Nov-2017) (Proof shortened by AV, 12-Nov-2024)

	Ref	Expression
Hypotheses	zlmlem2.1	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
	zlmtset.1	$$⊢J=\mathrm{TopSet}\left(G\right)$$
Assertion	zlmtset	$$⊢G\in V\to J=\mathrm{TopSet}\left(W\right)$$

Proof

Step	Hyp	Ref	Expression
1		zlmlem2.1	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
2		zlmtset.1	$$⊢J=\mathrm{TopSet}\left(G\right)$$
3		tsetid	$$⊢\mathrm{TopSet}=\mathrm{Slot}\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
4		slotstnscsi	$$⊢\left(\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)\wedge \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)\right)$$
5	4	simp1i	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
6	3 5	setsnid	$$⊢\mathrm{TopSet}\left(G\right)=\mathrm{TopSet}\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)$$
7	4	simp2i	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
8	3 7	setsnid	$$⊢\mathrm{TopSet}\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)=\mathrm{TopSet}\left(\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_G⟩\right)$$
9	2 6 8	3eqtri	$$⊢J=\mathrm{TopSet}\left(\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_G⟩\right)$$
10		eqid	$$⊢{\cdot }_G={\cdot }_G$$
11	1 10	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⟩$$
12	11	fveq2d	$$⊢G\in V\to \mathrm{TopSet}\left(W\right)=\mathrm{TopSet}\left(\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_G⟩\right)$$
13	9 12	eqtr4id	$$⊢G\in V\to J=\mathrm{TopSet}\left(W\right)$$