Theorem lmodring 20888

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 2740	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2740	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2740	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		lmodring.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
5		eqid 2740	. . 3 ⊢ (Base‘𝐹) = (Base‘𝐹)
6		eqid 2740	. . 3 ⊢ (+g‘𝐹) = (+g‘𝐹)
7		eqid 2740	. . 3 ⊢ (.r‘𝐹) = (.r‘𝐹)
8		eqid 2740	. . 3 ⊢ (1r‘𝐹) = (1r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20884	. 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ (Base‘𝐹)∀𝑟 ∈ (Base‘𝐹)∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠 ‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑥)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = ((𝑞( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = (𝑞( ·𝑠 ‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤)) ∧ ((1r‘𝐹)( ·𝑠 ‘𝑊)𝑤) = 𝑤))))
10	9	simp2bi 1146	1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  ∀wral 3067  ‘cfv 6573  (class class class)co 7448  Basecbs 17258  +_gcplusg 17311  ._rcmulr 17312  Scalarcsca 17314   ·_𝑠 cvsca 17315  Grpcgrp 18973  1_rcur 20208  Ringcrg 20260  LModclmod 20880

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-ral 3068  df-rab 3444  df-v 3490  df-sbc 3805  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-lmod 20882

This theorem is referenced by:  lmodfgrp  20889  lmodmcl  20893  lmod0cl  20908  lmod1cl  20909  lmod0vs  20915  lmodvs0  20916  lmodvsmmulgdi  20917  lmodvsneg  20926  lmodsubvs  20938  lmodsubdi  20939  lmodsubdir  20940  lssvnegcl  20977  islss3  20980  pwslmod  20991  lmodvsinv  21058  islmhm2  21060  lbsind2  21103  lspsneq  21147  lspexch  21154  ip2subdi  21685  isphld  21695  ocvlss  21713  frlmup1  21841  frlmup2  21842  frlmup3  21843  frlmup4  21844  islindf5  21882  lmisfree  21885  assasca  21905  asclghm  21926  ascl1  21928  ascldimul  21931  tlmtgp  24225  clmring  25122  lmodslmd  33183  imaslmod  33346  linds2eq  33374  lindsadd  37573  lfl0  39021  lfladd  39022  lflsub  39023  lfl0f  39025  lfladdcl  39027  lfladdcom  39028  lfladdass  39029  lfladd0l  39030  lflnegcl  39031  lflnegl  39032  lflvscl  39033  lflvsdi1  39034  lflvsdi2  39035  lflvsass  39037  lfl0sc  39038  lflsc0N  39039  lfl1sc  39040  lkrlss  39051  eqlkr  39055  eqlkr3  39057  lkrlsp  39058  ldualvsass  39097  lduallmodlem  39108  ldualvsubcl  39112  ldualvsubval  39113  lkrin  39120  dochfl1  41433  lcfl7lem  41456  lclkrlem2m  41476  lclkrlem2o  41478  lclkrlem2p  41479  lcfrlem1  41499  lcfrlem2  41500  lcfrlem3  41501  lcfrlem29  41528  lcfrlem33  41532  lcdvsubval  41575  mapdpglem30  41659  baerlem3lem1  41664  baerlem5alem1  41665  baerlem5blem1  41666  baerlem5blem2  41669  hgmapval1  41850  hdmapinvlem3  41877  hdmapinvlem4  41878  hdmapglem5  41879  hgmapvvlem1  41880  hdmapglem7b  41885  hdmapglem7  41886  lvecring  42493  prjspertr  42560  lmod0rng  47952  linc0scn0  48152  linc1  48154  lincscm  48159  lincscmcl  48161  el0ldep  48195  lindsrng01  48197  lindszr  48198  ldepsprlem  48201  ldepspr  48202  lincresunit3lem3  48203  lincresunitlem1  48204  lincresunitlem2  48205  lincresunit2  48207  lincresunit3lem1  48208