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

Theorem zlmvsca 20493
Description: Scalar multiplication operation of a -module. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypotheses
Ref Expression
zlmbas.w 𝑊 = (ℤMod‘𝐺)
zlmvsca.2 · = (.g𝐺)
Assertion
Ref Expression
zlmvsca · = ( ·𝑠𝑊)

Proof of Theorem zlmvsca
StepHypRef Expression
1 ovex 7251 . . . 4 (𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) ∈ V
2 zlmvsca.2 . . . . 5 · = (.g𝐺)
32fvexi 6736 . . . 4 · ∈ V
4 vscaid 16864 . . . . 5 ·𝑠 = Slot ( ·𝑠 ‘ndx)
54setsid 16763 . . . 4 (((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) ∈ V ∧ · ∈ V) → · = ( ·𝑠 ‘((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩)))
61, 3, 5mp2an 692 . . 3 · = ( ·𝑠 ‘((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩))
7 zlmbas.w . . . . 5 𝑊 = (ℤMod‘𝐺)
87, 2zlmval 20487 . . . 4 (𝐺 ∈ V → 𝑊 = ((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩))
98fveq2d 6726 . . 3 (𝐺 ∈ V → ( ·𝑠𝑊) = ( ·𝑠 ‘((𝐺 sSet ⟨(Scalar‘ndx), ℤring⟩) sSet ⟨( ·𝑠 ‘ndx), · ⟩)))
106, 9eqtr4id 2797 . 2 (𝐺 ∈ V → · = ( ·𝑠𝑊))
114str0 16747 . . 3 ∅ = ( ·𝑠 ‘∅)
12 fvprc 6714 . . . 4 𝐺 ∈ V → (.g𝐺) = ∅)
132, 12syl5eq 2790 . . 3 𝐺 ∈ V → · = ∅)
14 fvprc 6714 . . . . 5 𝐺 ∈ V → (ℤMod‘𝐺) = ∅)
157, 14syl5eq 2790 . . . 4 𝐺 ∈ V → 𝑊 = ∅)
1615fveq2d 6726 . . 3 𝐺 ∈ V → ( ·𝑠𝑊) = ( ·𝑠 ‘∅))
1711, 13, 163eqtr4a 2804 . 2 𝐺 ∈ V → · = ( ·𝑠𝑊))
1810, 17pm2.61i 185 1 · = ( ·𝑠𝑊)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1543  wcel 2110  Vcvv 3413  c0 4242  cop 4552  cfv 6385  (class class class)co 7218   sSet csts 16721  ndxcnx 16749  Scalarcsca 16810   ·𝑠 cvsca 16811  .gcmg 18493  ringzring 20440  ℤModczlm 20472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-cnex 10790  ax-1cn 10792  ax-addcl 10794
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-pred 6165  df-ord 6221  df-on 6222  df-lim 6223  df-suc 6224  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-ov 7221  df-oprab 7222  df-mpo 7223  df-om 7650  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-nn 11836  df-2 11898  df-3 11899  df-4 11900  df-5 11901  df-6 11902  df-sets 16722  df-slot 16740  df-ndx 16750  df-vsca 16824  df-zlm 20476
This theorem is referenced by:  zlmlmod  20494  zlmassa  20867  clmzlmvsca  24015  nmmulg  31635  cnzh  31637  rezh  31638
  Copyright terms: Public domain W3C validator