Theorem lmodring 20623

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.

Step	Hyp	Ref	Expression
1		eqid 2731	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2731	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2731	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		lmodring.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
5		eqid 2731	. . 3 ⊢ (Base‘𝐹) = (Base‘𝐹)
6		eqid 2731	. . 3 ⊢ (+g‘𝐹) = (+g‘𝐹)
7		eqid 2731	. . 3 ⊢ (.r‘𝐹) = (.r‘𝐹)
8		eqid 2731	. . 3 ⊢ (1r‘𝐹) = (1r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20619	. 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ (Base‘𝐹)∀𝑟 ∈ (Base‘𝐹)∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠 ‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑥)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = ((𝑞( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = (𝑞( ·𝑠 ‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤)) ∧ ((1r‘𝐹)( ·𝑠 ‘𝑊)𝑤) = 𝑤))))
10	9	simp2bi 1145	1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  ∀wral 3060  ‘cfv 6543  (class class class)co 7412  Basecbs 17149  +_gcplusg 17202  ._rcmulr 17203  Scalarcsca 17205   ·_𝑠 cvsca 17206  Grpcgrp 18856  1_rcur 20076  Ringcrg 20128  LModclmod 20615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-nul 5306

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-ne 2940  df-ral 3061  df-rab 3432  df-v 3475  df-sbc 3778  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-iota 6495  df-fv 6551  df-ov 7415  df-lmod 20617

This theorem is referenced by:  lmodfgrp  20624  lmodmcl  20628  lmod0cl  20643  lmod1cl  20644  lmod0vs  20650  lmodvs0  20651  lmodvsmmulgdi  20652  lmodvsneg  20661  lmodsubvs  20673  lmodsubdi  20674  lmodsubdir  20675  lssvnegcl  20712  islss3  20715  pwslmod  20726  lmodvsinv  20792  islmhm2  20794  lbsind2  20837  lspsneq  20881  lspexch  20888  ip2subdi  21417  isphld  21427  ocvlss  21445  frlmup1  21573  frlmup2  21574  frlmup3  21575  frlmup4  21576  islindf5  21614  lmisfree  21617  assasca  21637  asclghm  21657  ascl1  21659  ascldimul  21662  tlmtgp  23921  clmring  24818  lmodslmd  32620  imaslmod  32739  linds2eq  32772  lindsadd  36785  lfl0  38239  lfladd  38240  lflsub  38241  lfl0f  38243  lfladdcl  38245  lfladdcom  38246  lfladdass  38247  lfladd0l  38248  lflnegcl  38249  lflnegl  38250  lflvscl  38251  lflvsdi1  38252  lflvsdi2  38253  lflvsass  38255  lfl0sc  38256  lflsc0N  38257  lfl1sc  38258  lkrlss  38269  eqlkr  38273  eqlkr3  38275  lkrlsp  38276  ldualvsass  38315  lduallmodlem  38326  ldualvsubcl  38330  ldualvsubval  38331  lkrin  38338  dochfl1  40651  lcfl7lem  40674  lclkrlem2m  40694  lclkrlem2o  40696  lclkrlem2p  40697  lcfrlem1  40717  lcfrlem2  40718  lcfrlem3  40719  lcfrlem29  40746  lcfrlem33  40750  lcdvsubval  40793  mapdpglem30  40877  baerlem3lem1  40882  baerlem5alem1  40883  baerlem5blem1  40884  baerlem5blem2  40887  hgmapval1  41068  hdmapinvlem3  41095  hdmapinvlem4  41096  hdmapglem5  41097  hgmapvvlem1  41098  hdmapglem7b  41103  hdmapglem7  41104  lvecring  41411  prjspertr  41650  lmod0rng  46909  linc0scn0  47192  linc1  47194  lincscm  47199  lincscmcl  47201  el0ldep  47235  lindsrng01  47237  lindszr  47238  ldepsprlem  47241  ldepspr  47242  lincresunit3lem3  47243  lincresunitlem1  47244  lincresunitlem2  47245  lincresunit2  47247  lincresunit3lem1  47248