Theorem lmodring 20908

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095   = wceq 1554   ∈ wcel 2136  ∀wral 3070  ‘cfv 6510  (class class class)co 7385  Basecbs 17221  +_gcplusg 17262  ._rcmulr 17263  Scalarcsca 17265   ·_𝑠 cvsca 17266  Grpcgrp 18951  1_rcur 20203  Ringcrg 20255  LModclmod 20900

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-ext 2728  ax-nul 5250

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-sb 2085  df-clab 2735  df-cleq 2748  df-clel 2831  df-ne 2952  df-ral 3071  df-rab 3409  df-v 3450  df-sbc 3740  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4281  df-if 4475  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-iota 6466  df-fv 6518  df-ov 7388  df-lmod 20902

This theorem is referenced by:  lmodfgrp  20909  lmodmcl  20913  lmod0cl  20928  lmod1cl  20929  lmod0vs  20935  lmodvs0  20936  lmodvsmmulgdi  20937  lmodvsneg  20946  lmodsubvs  20958  lmodsubdi  20959  lmodsubdir  20960  lssvnegcl  20996  islss3  20999  pwslmod  21010  lmodvsinv  21076  islmhm2  21078  lbsind2  21121  lspsneq  21165  lspexch  21172  ip2subdi  21669  isphld  21679  ocvlss  21697  frlmup1  21823  frlmup2  21824  frlmup3  21825  frlmup4  21826  islindf5  21864  lmisfree  21867  assasca  21887  asclghm  21907  ascl1  21910  ascldimul  21913  tlmtgp  24229  clmring  25105  lmodslmd  33338  imaslmod  33493  linds2eq  33521  lindsadd  38060  lfl0  39637  lfladd  39638  lflsub  39639  lfl0f  39641  lfladdcl  39643  lfladdcom  39644  lfladdass  39645  lfladd0l  39646  lflnegcl  39647  lflnegl  39648  lflvscl  39649  lflvsdi1  39650  lflvsdi2  39651  lflvsass  39653  lfl0sc  39654  lflsc0N  39655  lfl1sc  39656  lkrlss  39667  eqlkr  39671  eqlkr3  39673  lkrlsp  39674  ldualvsass  39713  lduallmodlem  39724  ldualvsubcl  39728  ldualvsubval  39729  lkrin  39736  dochfl1  42048  lcfl7lem  42071  lclkrlem2m  42091  lclkrlem2o  42093  lclkrlem2p  42094  lcfrlem1  42114  lcfrlem2  42115  lcfrlem3  42116  lcfrlem29  42143  lcfrlem33  42147  lcdvsubval  42190  mapdpglem30  42274  baerlem3lem1  42279  baerlem5alem1  42280  baerlem5blem1  42281  baerlem5blem2  42284  hgmapval1  42465  hdmapinvlem3  42492  hdmapinvlem4  42493  hdmapglem5  42494  hgmapvvlem1  42495  hdmapglem7b  42500  hdmapglem7  42501  lvecring  43104  prjspertr  43135  lmod0rng  48799  linc0scn0  48993  linc1  48995  lincscm  49000  lincscmcl  49002  el0ldep  49036  lindsrng01  49038  lindszr  49039  ldepsprlem  49042  ldepspr  49043  lincresunit3lem3  49044  lincresunitlem1  49045  lincresunitlem2  49046  lincresunit2  49048  lincresunit3lem1  49049