Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  zlmval Structured version   Visualization version   GIF version

Theorem zlmval 20300
 Description: Augment an abelian group with vector space operations to turn it into a ℤ-module. (Contributed by Mario Carneiro, 2-Oct-2015.) (Revised by AV, 12-Jun-2019.)
Hypotheses
Ref Expression
zlmval.w 𝑊 = (ℤMod‘𝐺)
zlmval.m · = (.g𝐺)
Assertion
Ref Expression
zlmval (𝐺𝑉𝑊 = ((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩))

Proof of Theorem zlmval
Dummy variable 𝑔 is distinct from all other variables.
StepHypRef Expression
1 zlmval.w . 2 𝑊 = (ℤMod‘𝐺)
2 elex 3429 . . 3 (𝐺𝑉𝐺 ∈ V)
3 oveq1 7164 . . . . 5 (𝑔 = 𝐺 → (𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) = (𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩))
4 fveq2 6664 . . . . . . 7 (𝑔 = 𝐺 → (.g𝑔) = (.g𝐺))
5 zlmval.m . . . . . . 7 · = (.g𝐺)
64, 5eqtr4di 2812 . . . . . 6 (𝑔 = 𝐺 → (.g𝑔) = · )
76opeq2d 4774 . . . . 5 (𝑔 = 𝐺 → ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩ = ⟨( ·𝑠 ‘ndx), · ⟩)
83, 7oveq12d 7175 . . . 4 (𝑔 = 𝐺 → ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩) = ((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩))
9 df-zlm 20289 . . . 4 ℤMod = (𝑔 ∈ V ↦ ((𝑔 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), (.g𝑔)⟩))
10 ovex 7190 . . . 4 ((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩) ∈ V
118, 9, 10fvmpt 6765 . . 3 (𝐺 ∈ V → (ℤMod‘𝐺) = ((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩))
122, 11syl 17 . 2 (𝐺𝑉 → (ℤMod‘𝐺) = ((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩))
131, 12syl5eq 2806 1 (𝐺𝑉𝑊 = ((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2112  Vcvv 3410  ⟨cop 4532  ‘cfv 6341  (class class class)co 7157  ndxcnx 16553   sSet csts 16554  Scalarcsca 16641   ·𝑠 cvsca 16642  .gcmg 18306  ℤringzring 20253  ℤModczlm 20285 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5174  ax-nul 5181  ax-pr 5303 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ral 3076  df-rex 3077  df-v 3412  df-sbc 3700  df-dif 3864  df-un 3866  df-in 3868  df-ss 3878  df-nul 4229  df-if 4425  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4803  df-br 5038  df-opab 5100  df-mpt 5118  df-id 5435  df-xp 5535  df-rel 5536  df-cnv 5537  df-co 5538  df-dm 5539  df-iota 6300  df-fun 6343  df-fv 6349  df-ov 7160  df-zlm 20289 This theorem is referenced by:  zlmlem  20301  zlmsca  20305  zlmvsca  20306  zlmds  31447  zlmtset  31448
 Copyright terms: Public domain W3C validator