Theorem zlmds

Description: Distance 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)$$
	zlmds.1	$$⊢D=\mathrm{dist}\left(G\right)$$
Assertion	zlmds	$$⊢G\in V\to D=\mathrm{dist}\left(W\right)$$

Proof

Step	Hyp	Ref	Expression
1		zlmlem2.1	$$⊢W=\mathrm{\mathbb{Z}Mod}\left(G\right)$$
2		zlmds.1	$$⊢D=\mathrm{dist}\left(G\right)$$
3		eqid	$$⊢{\cdot }_G={\cdot }_G$$
4	1 3	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⟩$$
5	4	fveq2d	$$⊢G\in V\to \mathrm{dist}\left(W\right)=\mathrm{dist}\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		dsid	$$⊢\mathrm{dist}=\mathrm{Slot}\mathrm{dist}\left(\mathrm{ndx}\right)$$
7		5re	$$⊢5\in ℝ$$
8		1nn	$$⊢1\in \mathbb{N}$$
9		2nn0	$$⊢2\in {\mathbb{N}}_0$$
10		5nn0	$$⊢5\in {\mathbb{N}}_0$$
11		5lt10	$$⊢5<10$$
12	8 9 10 11	declti	$$⊢5<12$$
13	7 12	gtneii	$$⊢12\ne 5$$
14		dsndx	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)=12$$
15		scandx	$$⊢\mathrm{Scalar}\left(\mathrm{ndx}\right)=5$$
16	14 15	neeq12i	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)\leftrightarrow 12\ne 5$$
17	13 16	mpbir	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
18	6 17	setsnid	$$⊢\mathrm{dist}\left(G\right)=\mathrm{dist}\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)$$
19		6re	$$⊢6\in ℝ$$
20		6nn0	$$⊢6\in {\mathbb{N}}_0$$
21		6lt10	$$⊢6<10$$
22	8 9 20 21	declti	$$⊢6<12$$
23	19 22	gtneii	$$⊢12\ne 6$$
24		vscandx	$$⊢{\cdot }_{\mathrm{ndx}}=6$$
25	14 24	neeq12i	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\leftrightarrow 12\ne 6$$
26	23 25	mpbir	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
27	6 26	setsnid	$$⊢\mathrm{dist}\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)=\mathrm{dist}\left(\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_G⟩\right)$$
28	18 27	eqtri	$$⊢\mathrm{dist}\left(G\right)=\mathrm{dist}\left(\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)\mathrm{sSet}⟨{\cdot }_{\mathrm{ndx}},{\cdot }_G⟩\right)$$
29	5 28	eqtr4di	$$⊢G\in V\to \mathrm{dist}\left(W\right)=\mathrm{dist}\left(G\right)$$
30	2 29	eqtr4id	$$⊢G\in V\to D=\mathrm{dist}\left(W\right)$$