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	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
	zlmds.1	⊢ 𝐷 = ( dist ‘ 𝐺 )
Assertion	zlmds	⊢ ( 𝐺 ∈ 𝑉 → 𝐷 = ( dist ‘ 𝑊 ) )

Proof

Step	Hyp	Ref	Expression
1		zlmlem2.1	⊢ 𝑊 = ( ℤMod ‘ 𝐺 )
2		zlmds.1	⊢ 𝐷 = ( dist ‘ 𝐺 )
3		eqid	⊢ ( .g ‘ 𝐺 ) = ( .g ‘ 𝐺 )
4	1 3	zlmval	⊢ ( 𝐺 ∈ 𝑉 → 𝑊 = ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
5	4	fveq2d	⊢ ( 𝐺 ∈ 𝑉 → ( dist ‘ 𝑊 ) = ( dist ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) ) )
6		dsid	⊢ dist = Slot ( dist ‘ ndx )
7		slotsdnscsi	⊢ ( ( dist ‘ ndx ) ≠ ( Scalar ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( dist ‘ ndx ) ≠ ( ·𝑖 ‘ ndx ) )
8	7	simp1i	⊢ ( dist ‘ ndx ) ≠ ( Scalar ‘ ndx )
9	6 8	setsnid	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) )
10	7	simp2i	⊢ ( dist ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
11	6 10	setsnid	⊢ ( dist ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ) = ( dist ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
12	9 11	eqtri	⊢ ( dist ‘ 𝐺 ) = ( dist ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
13	5 12	eqtr4di	⊢ ( 𝐺 ∈ 𝑉 → ( dist ‘ 𝑊 ) = ( dist ‘ 𝐺 ) )
14	2 13	eqtr4id	⊢ ( 𝐺 ∈ 𝑉 → 𝐷 = ( dist ‘ 𝑊 ) )