Theorem lmodring 20865

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 20861	. 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ (Base‘𝐹)∀𝑟 ∈ (Base‘𝐹)∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠 ‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑥)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = ((𝑞( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = (𝑞( ·𝑠 ‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤)) ∧ ((1r‘𝐹)( ·𝑠 ‘𝑊)𝑤) = 𝑤))))
10	9	simp2bi 1152	1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3054  ‘cfv 6492  (class class class)co 7363  Basecbs 17177  +_gcplusg 17218  ._rcmulr 17219  Scalarcsca 17221   ·_𝑠 cvsca 17222  Grpcgrp 18907  1_rcur 20160  Ringcrg 20212  LModclmod 20857

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-iota 6448  df-fv 6500  df-ov 7366  df-lmod 20859

This theorem is referenced by:  lmodfgrp  20866  lmodmcl  20870  lmod0cl  20885  lmod1cl  20886  lmod0vs  20892  lmodvs0  20893  lmodvsmmulgdi  20894  lmodvsneg  20903  lmodsubvs  20915  lmodsubdi  20916  lmodsubdir  20917  lssvnegcl  20953  islss3  20956  pwslmod  20967  lmodvsinv  21033  islmhm2  21035  lbsind2  21078  lspsneq  21122  lspexch  21129  ip2subdi  21626  isphld  21636  ocvlss  21654  frlmup1  21780  frlmup2  21781  frlmup3  21782  frlmup4  21783  islindf5  21821  lmisfree  21824  assasca  21844  asclghm  21864  ascl1  21867  ascldimul  21870  tlmtgp  24186  clmring  25062  lmodslmd  33292  imaslmod  33443  linds2eq  33471  lindsadd  37981  lfl0  39558  lfladd  39559  lflsub  39560  lfl0f  39562  lfladdcl  39564  lfladdcom  39565  lfladdass  39566  lfladd0l  39567  lflnegcl  39568  lflnegl  39569  lflvscl  39570  lflvsdi1  39571  lflvsdi2  39572  lflvsass  39574  lfl0sc  39575  lflsc0N  39576  lfl1sc  39577  lkrlss  39588  eqlkr  39592  eqlkr3  39594  lkrlsp  39595  ldualvsass  39634  lduallmodlem  39645  ldualvsubcl  39649  ldualvsubval  39650  lkrin  39657  dochfl1  41969  lcfl7lem  41992  lclkrlem2m  42012  lclkrlem2o  42014  lclkrlem2p  42015  lcfrlem1  42035  lcfrlem2  42036  lcfrlem3  42037  lcfrlem29  42064  lcfrlem33  42068  lcdvsubval  42111  mapdpglem30  42195  baerlem3lem1  42200  baerlem5alem1  42201  baerlem5blem1  42202  baerlem5blem2  42205  hgmapval1  42386  hdmapinvlem3  42413  hdmapinvlem4  42414  hdmapglem5  42415  hgmapvvlem1  42416  hdmapglem7b  42421  hdmapglem7  42422  lvecring  43025  prjspertr  43056  lmod0rng  48721  linc0scn0  48915  linc1  48917  lincscm  48922  lincscmcl  48924  el0ldep  48958  lindsrng01  48960  lindszr  48961  ldepsprlem  48964  ldepspr  48965  lincresunit3lem3  48966  lincresunitlem1  48967  lincresunitlem2  48968  lincresunit2  48970  lincresunit3lem1  48971