Theorem lmodring 20622

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  ∀wral 3059  ‘cfv 6542  (class class class)co 7411  Basecbs 17148  +_gcplusg 17201  ._rcmulr 17202  Scalarcsca 17204   ·_𝑠 cvsca 17205  Grpcgrp 18855  1_rcur 20075  Ringcrg 20127  LModclmod 20614

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rab 3431  df-v 3474  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 6494  df-fv 6550  df-ov 7414  df-lmod 20616

This theorem is referenced by:  lmodfgrp  20623  lmodmcl  20627  lmod0cl  20642  lmod1cl  20643  lmod0vs  20649  lmodvs0  20650  lmodvsmmulgdi  20651  lmodvsneg  20660  lmodsubvs  20672  lmodsubdi  20673  lmodsubdir  20674  lssvnegcl  20711  islss3  20714  pwslmod  20725  lmodvsinv  20791  islmhm2  20793  lbsind2  20836  lspsneq  20880  lspexch  20887  ip2subdi  21416  isphld  21426  ocvlss  21444  frlmup1  21572  frlmup2  21573  frlmup3  21574  frlmup4  21575  islindf5  21613  lmisfree  21616  assasca  21636  asclghm  21656  ascl1  21658  ascldimul  21661  tlmtgp  23920  clmring  24817  lmodslmd  32619  imaslmod  32738  linds2eq  32771  lindsadd  36784  lfl0  38238  lfladd  38239  lflsub  38240  lfl0f  38242  lfladdcl  38244  lfladdcom  38245  lfladdass  38246  lfladd0l  38247  lflnegcl  38248  lflnegl  38249  lflvscl  38250  lflvsdi1  38251  lflvsdi2  38252  lflvsass  38254  lfl0sc  38255  lflsc0N  38256  lfl1sc  38257  lkrlss  38268  eqlkr  38272  eqlkr3  38274  lkrlsp  38275  ldualvsass  38314  lduallmodlem  38325  ldualvsubcl  38329  ldualvsubval  38330  lkrin  38337  dochfl1  40650  lcfl7lem  40673  lclkrlem2m  40693  lclkrlem2o  40695  lclkrlem2p  40696  lcfrlem1  40716  lcfrlem2  40717  lcfrlem3  40718  lcfrlem29  40745  lcfrlem33  40749  lcdvsubval  40792  mapdpglem30  40876  baerlem3lem1  40881  baerlem5alem1  40882  baerlem5blem1  40883  baerlem5blem2  40886  hgmapval1  41067  hdmapinvlem3  41094  hdmapinvlem4  41095  hdmapglem5  41096  hgmapvvlem1  41097  hdmapglem7b  41102  hdmapglem7  41103  lvecring  41410  prjspertr  41649  lmod0rng  46908  linc0scn0  47191  linc1  47193  lincscm  47198  lincscmcl  47200  el0ldep  47234  lindsrng01  47236  lindszr  47237  ldepsprlem  47240  ldepspr  47241  lincresunit3lem3  47242  lincresunitlem1  47243  lincresunitlem2  47244  lincresunit2  47246  lincresunit3lem1  47247