Theorem zlmds

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

	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		slotsdnscsi	$$⊢\left(\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{dist}\left(\mathrm{ndx}\right)\ne {\cdot }_{𝑖}\left(\mathrm{ndx}\right)\right)$$
8	7	simp1i	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{Scalar}\left(\mathrm{ndx}\right)$$
9	6 8	setsnid	$$⊢\mathrm{dist}\left(G\right)=\mathrm{dist}\left(G\mathrm{sSet}⟨\mathrm{Scalar}\left(\mathrm{ndx}\right),{\mathbb{Z}}_{\mathrm{ring}}⟩\right)$$
10	7	simp2i	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}$$
11	6 10	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)$$
12	9 11	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)$$
13	5 12	eqtr4di	$$⊢G\in V\to \mathrm{dist}\left(W\right)=\mathrm{dist}\left(G\right)$$
14	2 13	eqtr4id	$$⊢G\in V\to D=\mathrm{dist}\left(W\right)$$