Theorem zlmtset

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

	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		5re	$$⊢5\in ℝ$$
5		5lt9	$$⊢5<9$$
6	4 5	gtneii	$$⊢9\ne 5$$
7		tsetndx	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)=9$$
8		scandx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$$
9	7 8	neeq12i	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)\leftrightarrow 9\ne 5$$
10	6 9	mpbir	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
11	3 10	setsnid	$$⊢\mathrm{TopSet}\left(G\right)=\mathrm{TopSet}\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)$$
12		6re	$$⊢6\in ℝ$$
13		6lt9	$$⊢6<9$$
14	12 13	gtneii	$$⊢9\ne 6$$
15		vscandx	$$⊢{\cdot }_{\mathrm{ndx}}=6$$
16	7 15	neeq12i	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\leftrightarrow 9\ne 6$$
17	14 16	mpbir	$$⊢\mathrm{TopSet}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
18	3 17	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)$$
19	2 11 18	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)$$
20		eqid	$$⊢{\cdot }_G={\cdot }_G$$
21	1 20	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⟩$$
22	21	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)$$
23	19 22	eqtr4id	$$⊢G\in V\to J=\mathrm{TopSet}\left(W\right)$$