Theorem zlmds 30348

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

Hypotheses

Ref	Expression
zlmlem2.1	⊢ 𝑊 = (ℤMod‘𝐺)
zlmds.1	⊢ 𝐷 = (dist‘𝐺)

Assertion

Ref	Expression
zlmds	⊢ (𝐺 ∈ 𝑉 → 𝐷 = (dist‘𝑊))

Proof of Theorem zlmds

Step	Hyp	Ref	Expression
1		zlmlem2.1	. . . . 5 ⊢ 𝑊 = (ℤMod‘𝐺)
2		eqid 2771	. . . . 5 ⊢ (.g‘𝐺) = (.g‘𝐺)
3	1, 2	zlmval 20079	. . . 4 ⊢ (𝐺 ∈ 𝑉 → 𝑊 = ((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g‘𝐺)⟩))
4	3	fveq2d 6336	. . 3 ⊢ (𝐺 ∈ 𝑉 → (dist‘𝑊) = (dist‘((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g‘𝐺)⟩)))
5		dsid 16271	. . . . 5 ⊢ dist = Slot (dist‘ndx)
6		5re 11301	. . . . . . 7 ⊢ 5 ∈ ℝ
7		1nn 11233	. . . . . . . 8 ⊢ 1 ∈ ℕ
8		2nn0 11511	. . . . . . . 8 ⊢ 2 ∈ ℕ0
9		5nn0 11514	. . . . . . . 8 ⊢ 5 ∈ ℕ0
10		5lt10 11878	. . . . . . . 8 ⊢ 5 < ;10
11	7, 8, 9, 10	declti 11748	. . . . . . 7 ⊢ 5 < ;12
12	6, 11	gtneii 10351	. . . . . 6 ⊢ ;12 ≠ 5
13		dsndx 16270	. . . . . . 7 ⊢ (dist‘ndx) = ;12
14		scandx 16221	. . . . . . 7 ⊢ (Scalar‘ndx) = 5
15	13, 14	neeq12i 3009	. . . . . 6 ⊢ ((dist‘ndx) ≠ (Scalar‘ndx) ↔ ;12 ≠ 5)
16	12, 15	mpbir 221	. . . . 5 ⊢ (dist‘ndx) ≠ (Scalar‘ndx)
17	5, 16	setsnid 16122	. . . 4 ⊢ (dist‘𝐺) = (dist‘(𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩))
18		6re 11303	. . . . . . 7 ⊢ 6 ∈ ℝ
19		6nn0 11515	. . . . . . . 8 ⊢ 6 ∈ ℕ0
20		6lt10 11877	. . . . . . . 8 ⊢ 6 < ;10
21	7, 8, 19, 20	declti 11748	. . . . . . 7 ⊢ 6 < ;12
22	18, 21	gtneii 10351	. . . . . 6 ⊢ ;12 ≠ 6
23		vscandx 16223	. . . . . . 7 ⊢ ( ·𝑠 ‘ndx) = 6
24	13, 23	neeq12i 3009	. . . . . 6 ⊢ ((dist‘ndx) ≠ ( ·𝑠 ‘ndx) ↔ ;12 ≠ 6)
25	22, 24	mpbir 221	. . . . 5 ⊢ (dist‘ndx) ≠ ( ·𝑠 ‘ndx)
26	5, 25	setsnid 16122	. . . 4 ⊢ (dist‘(𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩)) = (dist‘((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g‘𝐺)⟩))
27	17, 26	eqtri 2793	. . 3 ⊢ (dist‘𝐺) = (dist‘((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g‘𝐺)⟩))
28	4, 27	syl6eqr 2823	. 2 ⊢ (𝐺 ∈ 𝑉 → (dist‘𝑊) = (dist‘𝐺))
29		zlmds.1	. 2 ⊢ 𝐷 = (dist‘𝐺)
30	28, 29	syl6reqr 2824	1 ⊢ (𝐺 ∈ 𝑉 → 𝐷 = (dist‘𝑊))

Syntax hints:   → wi 4   = wceq 1631   ∈ wcel 2145   ≠ wne 2943  ⟨cop 4322  ‘cfv 6031  (class class class)co 6793  1c1 10139  2c2 11272  5c5 11275  6c6 11276  ;cdc 11695  ndxcnx 16061   sSet csts 16062  Scalarcsca 16152   ·_𝑠 cvsca 16153  distcds 16158  ._gcmg 17748  ℤ_ringzring 20033  ℤModczlm 20064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-ndx 16067  df-slot 16068  df-sets 16071  df-sca 16165  df-vsca 16166  df-ds 16172  df-zlm 20068

This theorem is referenced by:  zlmnm  30350  zhmnrg  30351