Theorem lmodring 21105

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145  ∀wral 3076  ‘cfv 6527  (class class class)co 7408  Basecbs 17349  +_gcplusg 17390  ._rcmulr 17391  Scalarcsca 17393   ·_𝑠 cvsca 17394  Grpcgrp 19106  1_rcur 20369  Ringcrg 20421  LModclmod 21097

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rab 3413  df-v 3452  df-sbc 3739  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6483  df-fv 6535  df-ov 7411  df-lmod 21099

This theorem is used by:  lmodfgrp  21106  lmodmcl  21110  lmod0cl  21125  lmod1cl  21126  lmod0vs  21132  lmodvs0  21133  lmodvsmmulgdi  21134  lmodvsneg  21143  lmodsubvs  21155  lmodsubdi  21156  lmodsubdir  21157  lssvnegcl  21193  islss3  21196  pwslmod  21207  lmodvsinv  21273  islmhm2  21275  lbsind2  21318  lspsneq  21362  lspexch  21369  ip2subdi  21912  isphld  21922  ocvlss  21940  frlmup1  22066  frlmup2  22067  frlmup3  22068  frlmup4  22069  islindf5  22107  lmisfree  22110  assasca  22132  asclghm  22152  ascl1  22155  tlmtgp  24477  clmring  25353  lmodslmd  33699  imaslmod  33848  linds2eq  33870  lindsadd  38456  lfl0  40042  lfladd  40043  lflsub  40044  lfl0f  40046  lfladdcl  40048  lfladdcom  40049  lfladdass  40050  lfladd0l  40051  lflnegcl  40052  lflnegl  40053  lflvscl  40054  lflvsdi1  40055  lflvsdi2  40056  lflvsass  40058  lfl0sc  40059  lflsc0N  40060  lfl1sc  40061  lkrlss  40072  eqlkr  40076  eqlkr3  40078  lkrlsp  40079  ldualvsass  40118  lduallmodlem  40129  ldualvsubcl  40133  ldualvsubval  40134  lkrin  40141  dochfl1  42453  lcfl7lem  42476  lclkrlem2m  42496  lclkrlem2o  42498  lclkrlem2p  42499  lcfrlem1  42519  lcfrlem2  42520  lcfrlem3  42521  lcfrlem29  42548  lcfrlem33  42552  lcdvsubval  42595  mapdpglem30  42679  baerlem3lem1  42684  baerlem5alem1  42685  baerlem5blem1  42686  baerlem5blem2  42689  hgmapval1  42870  hdmapinvlem3  42897  hdmapinvlem4  42898  hdmapglem5  42899  hgmapvvlem1  42900  hdmapglem7b  42905  hdmapglem7  42906  lvecring  43524  prjspertr  43555  lmod0rng  49248  linc0scn0  49457  linc1  49459  lincscm  49464  lincscmcl  49466  el0ldep  49500  lindsrng01  49502  lindszr  49503  ldepsprlem  49506  ldepspr  49507  lincresunit3lem3  49508  lincresunitlem1  49509  lincresunitlem2  49510  lincresunit2  49512  lincresunit3lem1  49513