Theorem lmodring 20471

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 2732	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2732	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2732	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		lmodring.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
5		eqid 2732	. . 3 ⊢ (Base‘𝐹) = (Base‘𝐹)
6		eqid 2732	. . 3 ⊢ (+g‘𝐹) = (+g‘𝐹)
7		eqid 2732	. . 3 ⊢ (.r‘𝐹) = (.r‘𝐹)
8		eqid 2732	. . 3 ⊢ (1r‘𝐹) = (1r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20467	. 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 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  ∀wral 3061  ‘cfv 6540  (class class class)co 7405  Basecbs 17140  +_gcplusg 17193  ._rcmulr 17194  Scalarcsca 17196   ·_𝑠 cvsca 17197  Grpcgrp 18815  1_rcur 19998  Ringcrg 20049  LModclmod 20463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rab 3433  df-v 3476  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6492  df-fv 6548  df-ov 7408  df-lmod 20465

This theorem is referenced by:  lmodfgrp  20472  lmodmcl  20476  lmod0cl  20490  lmod1cl  20491  lmod0vs  20497  lmodvs0  20498  lmodvsmmulgdi  20499  lmodvsneg  20508  lmodsubvs  20520  lmodsubdi  20521  lmodsubdir  20522  lssvnegcl  20559  islss3  20562  pwslmod  20573  lmodvsinv  20639  islmhm2  20641  lbsind2  20684  lspsneq  20727  lspexch  20734  ip2subdi  21188  isphld  21198  ocvlss  21216  frlmup1  21344  frlmup2  21345  frlmup3  21346  frlmup4  21347  islindf5  21385  lmisfree  21388  assasca  21408  asclghm  21428  ascl1  21430  ascldimul  21433  tlmtgp  23691  clmring  24577  lmodslmd  32336  imaslmod  32456  linds2eq  32485  lindsadd  36469  lfl0  37923  lfladd  37924  lflsub  37925  lfl0f  37927  lfladdcl  37929  lfladdcom  37930  lfladdass  37931  lfladd0l  37932  lflnegcl  37933  lflnegl  37934  lflvscl  37935  lflvsdi1  37936  lflvsdi2  37937  lflvsass  37939  lfl0sc  37940  lflsc0N  37941  lfl1sc  37942  lkrlss  37953  eqlkr  37957  eqlkr3  37959  lkrlsp  37960  ldualvsass  37999  lduallmodlem  38010  ldualvsubcl  38014  ldualvsubval  38015  lkrin  38022  dochfl1  40335  lcfl7lem  40358  lclkrlem2m  40378  lclkrlem2o  40380  lclkrlem2p  40381  lcfrlem1  40401  lcfrlem2  40402  lcfrlem3  40403  lcfrlem29  40430  lcfrlem33  40434  lcdvsubval  40477  mapdpglem30  40561  baerlem3lem1  40566  baerlem5alem1  40567  baerlem5blem1  40568  baerlem5blem2  40571  hgmapval1  40752  hdmapinvlem3  40779  hdmapinvlem4  40780  hdmapglem5  40781  hgmapvvlem1  40782  hdmapglem7b  40787  hdmapglem7  40788  lvecring  41105  prjspertr  41343  lmod0rng  46628  linc0scn0  47057  linc1  47059  lincscm  47064  lincscmcl  47066  el0ldep  47100  lindsrng01  47102  lindszr  47103  ldepsprlem  47106  ldepspr  47107  lincresunit3lem3  47108  lincresunitlem1  47109  lincresunitlem2  47110  lincresunit2  47112  lincresunit3lem1  47113