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

Theorem lmodring 19635
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 2798 . . 3 (Base‘𝑊) = (Base‘𝑊)
2 eqid 2798 . . 3 (+g𝑊) = (+g𝑊)
3 eqid 2798 . . 3 ( ·𝑠𝑊) = ( ·𝑠𝑊)
4 lmodring.1 . . 3 𝐹 = (Scalar‘𝑊)
5 eqid 2798 . . 3 (Base‘𝐹) = (Base‘𝐹)
6 eqid 2798 . . 3 (+g𝐹) = (+g𝐹)
7 eqid 2798 . . 3 (.r𝐹) = (.r𝐹)
8 eqid 2798 . . 3 (1r𝐹) = (1r𝐹)
91, 2, 3, 4, 5, 6, 7, 8islmod 19631 . 2 (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ (Base‘𝐹)∀𝑟 ∈ (Base‘𝐹)∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠𝑊)(𝑤(+g𝑊)𝑥)) = ((𝑟( ·𝑠𝑊)𝑤)(+g𝑊)(𝑟( ·𝑠𝑊)𝑥)) ∧ ((𝑞(+g𝐹)𝑟)( ·𝑠𝑊)𝑤) = ((𝑞( ·𝑠𝑊)𝑤)(+g𝑊)(𝑟( ·𝑠𝑊)𝑤))) ∧ (((𝑞(.r𝐹)𝑟)( ·𝑠𝑊)𝑤) = (𝑞( ·𝑠𝑊)(𝑟( ·𝑠𝑊)𝑤)) ∧ ((1r𝐹)( ·𝑠𝑊)𝑤) = 𝑤))))
109simp2bi 1143 1 (𝑊 ∈ LMod → 𝐹 ∈ Ring)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  w3a 1084   = wceq 1538  wcel 2111  wral 3106  cfv 6324  (class class class)co 7135  Basecbs 16475  +gcplusg 16557  .rcmulr 16558  Scalarcsca 16560   ·𝑠 cvsca 16561  Grpcgrp 18095  1rcur 19244  Ringcrg 19290  LModclmod 19627
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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5174
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-lmod 19629
This theorem is referenced by:  lmodfgrp  19636  lmodmcl  19639  lmod0cl  19653  lmod1cl  19654  lmod0vs  19660  lmodvs0  19661  lmodvsmmulgdi  19662  lmodvsneg  19671  lmodsubvs  19683  lmodsubdi  19684  lmodsubdir  19685  lssvnegcl  19721  islss3  19724  pwslmod  19735  lmodvsinv  19801  islmhm2  19803  lbsind2  19846  lspsneq  19887  lspexch  19894  ip2subdi  20333  isphld  20343  ocvlss  20361  frlmup1  20487  frlmup2  20488  frlmup3  20489  frlmup4  20490  islindf5  20528  lmisfree  20531  asclghm  20569  ascldimul  20573  tlmtgp  22801  clmring  23675  lmodslmd  30882  imaslmod  30973  linds2eq  30995  lindsadd  35047  lfl0  36358  lfladd  36359  lflsub  36360  lfl0f  36362  lfladdcl  36364  lfladdcom  36365  lfladdass  36366  lfladd0l  36367  lflnegcl  36368  lflnegl  36369  lflvscl  36370  lflvsdi1  36371  lflvsdi2  36372  lflvsass  36374  lfl0sc  36375  lflsc0N  36376  lfl1sc  36377  lkrlss  36388  eqlkr  36392  eqlkr3  36394  lkrlsp  36395  ldualvsass  36434  lduallmodlem  36445  ldualvsubcl  36449  ldualvsubval  36450  lkrin  36457  dochfl1  38769  lcfl7lem  38792  lclkrlem2m  38812  lclkrlem2o  38814  lclkrlem2p  38815  lcfrlem1  38835  lcfrlem2  38836  lcfrlem3  38837  lcfrlem29  38864  lcfrlem33  38868  lcdvsubval  38911  mapdpglem30  38995  baerlem3lem1  39000  baerlem5alem1  39001  baerlem5blem1  39002  baerlem5blem2  39005  hgmapval1  39186  hdmapinvlem3  39213  hdmapinvlem4  39214  hdmapglem5  39215  hgmapvvlem1  39216  hdmapglem7b  39221  hdmapglem7  39222  lvecring  39446  prjspertr  39594  lmod0rng  44487  ascl1  44781  linc0scn0  44827  linc1  44829  lincscm  44834  lincscmcl  44836  el0ldep  44870  lindsrng01  44872  lindszr  44873  ldepsprlem  44876  ldepspr  44877  lincresunit3lem3  44878  lincresunitlem1  44879  lincresunitlem2  44880  lincresunit2  44882  lincresunit3lem1  44883
  Copyright terms: Public domain W3C validator