Theorem lmodring 20844

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084   = wceq 1534   ∈ wcel 2099  ∀wral 3051  ‘cfv 6554  (class class class)co 7424  Basecbs 17213  +_gcplusg 17266  ._rcmulr 17267  Scalarcsca 17269   ·_𝑠 cvsca 17270  Grpcgrp 18928  1_rcur 20164  Ringcrg 20216  LModclmod 20836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-nul 5311

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-ne 2931  df-ral 3052  df-rab 3420  df-v 3464  df-sbc 3777  df-dif 3950  df-un 3952  df-ss 3964  df-nul 4326  df-if 4534  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-br 5154  df-iota 6506  df-fv 6562  df-ov 7427  df-lmod 20838

This theorem is referenced by:  lmodfgrp  20845  lmodmcl  20849  lmod0cl  20864  lmod1cl  20865  lmod0vs  20871  lmodvs0  20872  lmodvsmmulgdi  20873  lmodvsneg  20882  lmodsubvs  20894  lmodsubdi  20895  lmodsubdir  20896  lssvnegcl  20933  islss3  20936  pwslmod  20947  lmodvsinv  21014  islmhm2  21016  lbsind2  21059  lspsneq  21103  lspexch  21110  ip2subdi  21640  isphld  21650  ocvlss  21668  frlmup1  21796  frlmup2  21797  frlmup3  21798  frlmup4  21799  islindf5  21837  lmisfree  21840  assasca  21860  asclghm  21880  ascl1  21882  ascldimul  21885  tlmtgp  24191  clmring  25088  lmodslmd  33068  imaslmod  33228  linds2eq  33256  lindsadd  37314  lfl0  38763  lfladd  38764  lflsub  38765  lfl0f  38767  lfladdcl  38769  lfladdcom  38770  lfladdass  38771  lfladd0l  38772  lflnegcl  38773  lflnegl  38774  lflvscl  38775  lflvsdi1  38776  lflvsdi2  38777  lflvsass  38779  lfl0sc  38780  lflsc0N  38781  lfl1sc  38782  lkrlss  38793  eqlkr  38797  eqlkr3  38799  lkrlsp  38800  ldualvsass  38839  lduallmodlem  38850  ldualvsubcl  38854  ldualvsubval  38855  lkrin  38862  dochfl1  41175  lcfl7lem  41198  lclkrlem2m  41218  lclkrlem2o  41220  lclkrlem2p  41221  lcfrlem1  41241  lcfrlem2  41242  lcfrlem3  41243  lcfrlem29  41270  lcfrlem33  41274  lcdvsubval  41317  mapdpglem30  41401  baerlem3lem1  41406  baerlem5alem1  41407  baerlem5blem1  41408  baerlem5blem2  41411  hgmapval1  41592  hdmapinvlem3  41619  hdmapinvlem4  41620  hdmapglem5  41621  hgmapvvlem1  41622  hdmapglem7b  41627  hdmapglem7  41628  lvecring  42010  prjspertr  42259  lmod0rng  47606  linc0scn0  47806  linc1  47808  lincscm  47813  lincscmcl  47815  el0ldep  47849  lindsrng01  47851  lindszr  47852  ldepsprlem  47855  ldepspr  47856  lincresunit3lem3  47857  lincresunitlem1  47858  lincresunitlem2  47859  lincresunit2  47861  lincresunit3lem1  47862