Theorem lmodring 19861

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089   = wceq 1543   ∈ wcel 2112  ∀wral 3051  ‘cfv 6358  (class class class)co 7191  Basecbs 16666  +_gcplusg 16749  ._rcmulr 16750  Scalarcsca 16752   ·_𝑠 cvsca 16753  Grpcgrp 18319  1_rcur 19470  Ringcrg 19516  LModclmod 19853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-nul 5184

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366  df-ov 7194  df-lmod 19855

This theorem is referenced by:  lmodfgrp  19862  lmodmcl  19865  lmod0cl  19879  lmod1cl  19880  lmod0vs  19886  lmodvs0  19887  lmodvsmmulgdi  19888  lmodvsneg  19897  lmodsubvs  19909  lmodsubdi  19910  lmodsubdir  19911  lssvnegcl  19947  islss3  19950  pwslmod  19961  lmodvsinv  20027  islmhm2  20029  lbsind2  20072  lspsneq  20113  lspexch  20120  ip2subdi  20560  isphld  20570  ocvlss  20588  frlmup1  20714  frlmup2  20715  frlmup3  20716  frlmup4  20717  islindf5  20755  lmisfree  20758  asclghm  20796  ascl1  20798  ascldimul  20801  tlmtgp  23047  clmring  23921  lmodslmd  31130  imaslmod  31221  linds2eq  31243  lindsadd  35456  lfl0  36765  lfladd  36766  lflsub  36767  lfl0f  36769  lfladdcl  36771  lfladdcom  36772  lfladdass  36773  lfladd0l  36774  lflnegcl  36775  lflnegl  36776  lflvscl  36777  lflvsdi1  36778  lflvsdi2  36779  lflvsass  36781  lfl0sc  36782  lflsc0N  36783  lfl1sc  36784  lkrlss  36795  eqlkr  36799  eqlkr3  36801  lkrlsp  36802  ldualvsass  36841  lduallmodlem  36852  ldualvsubcl  36856  ldualvsubval  36857  lkrin  36864  dochfl1  39176  lcfl7lem  39199  lclkrlem2m  39219  lclkrlem2o  39221  lclkrlem2p  39222  lcfrlem1  39242  lcfrlem2  39243  lcfrlem3  39244  lcfrlem29  39271  lcfrlem33  39275  lcdvsubval  39318  mapdpglem30  39402  baerlem3lem1  39407  baerlem5alem1  39408  baerlem5blem1  39409  baerlem5blem2  39412  hgmapval1  39593  hdmapinvlem3  39620  hdmapinvlem4  39621  hdmapglem5  39622  hgmapvvlem1  39623  hdmapglem7b  39628  hdmapglem7  39629  lvecring  39913  prjspertr  40093  lmod0rng  45042  linc0scn0  45380  linc1  45382  lincscm  45387  lincscmcl  45389  el0ldep  45423  lindsrng01  45425  lindszr  45426  ldepsprlem  45429  ldepspr  45430  lincresunit3lem3  45431  lincresunitlem1  45432  lincresunitlem2  45433  lincresunit2  45435  lincresunit3lem1  45436