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

Theorem lmodring 20330
Description: The scalar component of a left module is a ring. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.)
Hypothesis
Ref Expression
lmodring.1 𝐹 = (Scalarβ€˜π‘Š)
Assertion
Ref Expression
lmodring (π‘Š ∈ LMod β†’ 𝐹 ∈ Ring)

Proof of Theorem lmodring
Dummy variables π‘Ÿ π‘ž 𝑀 π‘₯ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2736 . . 3 (Baseβ€˜π‘Š) = (Baseβ€˜π‘Š)
2 eqid 2736 . . 3 (+gβ€˜π‘Š) = (+gβ€˜π‘Š)
3 eqid 2736 . . 3 ( ·𝑠 β€˜π‘Š) = ( ·𝑠 β€˜π‘Š)
4 lmodring.1 . . 3 𝐹 = (Scalarβ€˜π‘Š)
5 eqid 2736 . . 3 (Baseβ€˜πΉ) = (Baseβ€˜πΉ)
6 eqid 2736 . . 3 (+gβ€˜πΉ) = (+gβ€˜πΉ)
7 eqid 2736 . . 3 (.rβ€˜πΉ) = (.rβ€˜πΉ)
8 eqid 2736 . . 3 (1rβ€˜πΉ) = (1rβ€˜πΉ)
91, 2, 3, 4, 5, 6, 7, 8islmod 20326 . 2 (π‘Š ∈ LMod ↔ (π‘Š ∈ Grp ∧ 𝐹 ∈ Ring ∧ βˆ€π‘ž ∈ (Baseβ€˜πΉ)βˆ€π‘Ÿ ∈ (Baseβ€˜πΉ)βˆ€π‘₯ ∈ (Baseβ€˜π‘Š)βˆ€π‘€ ∈ (Baseβ€˜π‘Š)(((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀) ∈ (Baseβ€˜π‘Š) ∧ (π‘Ÿ( ·𝑠 β€˜π‘Š)(𝑀(+gβ€˜π‘Š)π‘₯)) = ((π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)π‘₯)) ∧ ((π‘ž(+gβ€˜πΉ)π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = ((π‘ž( ·𝑠 β€˜π‘Š)𝑀)(+gβ€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀))) ∧ (((π‘ž(.rβ€˜πΉ)π‘Ÿ)( ·𝑠 β€˜π‘Š)𝑀) = (π‘ž( ·𝑠 β€˜π‘Š)(π‘Ÿ( ·𝑠 β€˜π‘Š)𝑀)) ∧ ((1rβ€˜πΉ)( ·𝑠 β€˜π‘Š)𝑀) = 𝑀))))
109simp2bi 1146 1 (π‘Š ∈ LMod β†’ 𝐹 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆ€wral 3064  β€˜cfv 6496  (class class class)co 7357  Basecbs 17083  +gcplusg 17133  .rcmulr 17134  Scalarcsca 17136   ·𝑠 cvsca 17137  Grpcgrp 18748  1rcur 19913  Ringcrg 19964  LModclmod 20322
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-nul 5263
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7360  df-lmod 20324
This theorem is referenced by:  lmodfgrp  20331  lmodmcl  20334  lmod0cl  20348  lmod1cl  20349  lmod0vs  20355  lmodvs0  20356  lmodvsmmulgdi  20357  lmodvsneg  20366  lmodsubvs  20378  lmodsubdi  20379  lmodsubdir  20380  lssvnegcl  20417  islss3  20420  pwslmod  20431  lmodvsinv  20497  islmhm2  20499  lbsind2  20542  lspsneq  20583  lspexch  20590  ip2subdi  21048  isphld  21058  ocvlss  21076  frlmup1  21204  frlmup2  21205  frlmup3  21206  frlmup4  21207  islindf5  21245  lmisfree  21248  asclghm  21286  ascl1  21288  ascldimul  21291  tlmtgp  23547  clmring  24433  lmodslmd  32039  imaslmod  32145  linds2eq  32168  lindsadd  36071  lfl0  37527  lfladd  37528  lflsub  37529  lfl0f  37531  lfladdcl  37533  lfladdcom  37534  lfladdass  37535  lfladd0l  37536  lflnegcl  37537  lflnegl  37538  lflvscl  37539  lflvsdi1  37540  lflvsdi2  37541  lflvsass  37543  lfl0sc  37544  lflsc0N  37545  lfl1sc  37546  lkrlss  37557  eqlkr  37561  eqlkr3  37563  lkrlsp  37564  ldualvsass  37603  lduallmodlem  37614  ldualvsubcl  37618  ldualvsubval  37619  lkrin  37626  dochfl1  39939  lcfl7lem  39962  lclkrlem2m  39982  lclkrlem2o  39984  lclkrlem2p  39985  lcfrlem1  40005  lcfrlem2  40006  lcfrlem3  40007  lcfrlem29  40034  lcfrlem33  40038  lcdvsubval  40081  mapdpglem30  40165  baerlem3lem1  40170  baerlem5alem1  40171  baerlem5blem1  40172  baerlem5blem2  40175  hgmapval1  40356  hdmapinvlem3  40383  hdmapinvlem4  40384  hdmapglem5  40385  hgmapvvlem1  40386  hdmapglem7b  40391  hdmapglem7  40392  lvecring  40713  prjspertr  40929  lmod0rng  46156  linc0scn0  46494  linc1  46496  lincscm  46501  lincscmcl  46503  el0ldep  46537  lindsrng01  46539  lindszr  46540  ldepsprlem  46543  ldepspr  46544  lincresunit3lem3  46545  lincresunitlem1  46546  lincresunitlem2  46547  lincresunit2  46549  lincresunit3lem1  46550
  Copyright terms: Public domain W3C validator