Metamath Proof Explorer

Theorem zlmds

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

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 5re ⊢ 5 ∈ ℝ
8 1nn ⊢ 1 ∈ ℕ
9 2nn0 ⊢ 2 ∈ ℕ0
10 5nn0 ⊢ 5 ∈ ℕ0
11 5lt10 ⊢ 5 < 1 0
12 8 9 10 11 declti ⊢ 5 < 1 2
13 7 12 gtneii ⊢ 1 2 ≠ 5
14 dsndx ⊢ ( dist ‘ ndx ) = 1 2
15 scandx ⊢ ( Scalar ‘ ndx ) = 5
16 14 15 neeq12i ⊢ ( ( dist ‘ ndx ) ≠ ( Scalar ‘ ndx ) ↔ 1 2 ≠ 5 )
17 13 16 mpbir ⊢ ( dist ‘ ndx ) ≠ ( Scalar ‘ ndx )
18 6 17 setsnid ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) )
19 6re ⊢ 6 ∈ ℝ
20 6nn0 ⊢ 6 ∈ ℕ0
21 6lt10 ⊢ 6 < 1 0
22 8 9 20 21 declti ⊢ 6 < 1 2
23 19 22 gtneii ⊢ 1 2 ≠ 6
24 vscandx ⊢ ( ·𝑠 ‘ ndx ) = 6
25 14 24 neeq12i ⊢ ( ( dist ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ↔ 1 2 ≠ 6 )
26 23 25 mpbir ⊢ ( dist ‘ ndx ) ≠ ( ·𝑠 ‘ ndx )
27 6 26 setsnid ⊢ ( dist ‘ ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) ) = ( dist ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
28 18 27 eqtri ⊢ ( dist ‘ 𝐺 ) = ( dist ‘ ( ( 𝐺 sSet ⟨ ( Scalar ‘ ndx ) , ℤring ⟩ ) sSet ⟨ ( ·𝑠 ‘ ndx ) , ( .g ‘ 𝐺 ) ⟩ ) )
29 5 28 eqtr4di ⊢ ( 𝐺 ∈ 𝑉 → ( dist ‘ 𝑊 ) = ( dist ‘ 𝐺 ) )
30 2 29 eqtr4id ⊢ ( 𝐺 ∈ 𝑉 → 𝐷 = ( dist ‘ 𝑊 ) )