Theorem lmodring 20774

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 2729	. . 3 ⊢ (Base‘𝑊) = (Base‘𝑊)
2		eqid 2729	. . 3 ⊢ (+g‘𝑊) = (+g‘𝑊)
3		eqid 2729	. . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊)
4		lmodring.1	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
5		eqid 2729	. . 3 ⊢ (Base‘𝐹) = (Base‘𝐹)
6		eqid 2729	. . 3 ⊢ (+g‘𝐹) = (+g‘𝐹)
7		eqid 2729	. . 3 ⊢ (.r‘𝐹) = (.r‘𝐹)
8		eqid 2729	. . 3 ⊢ (1r‘𝐹) = (1r‘𝐹)
9	1, 2, 3, 4, 5, 6, 7, 8	islmod 20770	. 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 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ‘cfv 6511  (class class class)co 7387  Basecbs 17179  +_gcplusg 17220  ._rcmulr 17221  Scalarcsca 17223   ·_𝑠 cvsca 17224  Grpcgrp 18865  1_rcur 20090  Ringcrg 20142  LModclmod 20766

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5261

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3406  df-v 3449  df-sbc 3754  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-lmod 20768

This theorem is referenced by:  lmodfgrp  20775  lmodmcl  20779  lmod0cl  20794  lmod1cl  20795  lmod0vs  20801  lmodvs0  20802  lmodvsmmulgdi  20803  lmodvsneg  20812  lmodsubvs  20824  lmodsubdi  20825  lmodsubdir  20826  lssvnegcl  20862  islss3  20865  pwslmod  20876  lmodvsinv  20943  islmhm2  20945  lbsind2  20988  lspsneq  21032  lspexch  21039  ip2subdi  21553  isphld  21563  ocvlss  21581  frlmup1  21707  frlmup2  21708  frlmup3  21709  frlmup4  21710  islindf5  21748  lmisfree  21751  assasca  21771  asclghm  21792  ascl1  21794  ascldimul  21797  tlmtgp  24083  clmring  24970  lmodslmd  33157  imaslmod  33324  linds2eq  33352  lindsadd  37607  lfl0  39058  lfladd  39059  lflsub  39060  lfl0f  39062  lfladdcl  39064  lfladdcom  39065  lfladdass  39066  lfladd0l  39067  lflnegcl  39068  lflnegl  39069  lflvscl  39070  lflvsdi1  39071  lflvsdi2  39072  lflvsass  39074  lfl0sc  39075  lflsc0N  39076  lfl1sc  39077  lkrlss  39088  eqlkr  39092  eqlkr3  39094  lkrlsp  39095  ldualvsass  39134  lduallmodlem  39145  ldualvsubcl  39149  ldualvsubval  39150  lkrin  39157  dochfl1  41470  lcfl7lem  41493  lclkrlem2m  41513  lclkrlem2o  41515  lclkrlem2p  41516  lcfrlem1  41536  lcfrlem2  41537  lcfrlem3  41538  lcfrlem29  41565  lcfrlem33  41569  lcdvsubval  41612  mapdpglem30  41696  baerlem3lem1  41701  baerlem5alem1  41702  baerlem5blem1  41703  baerlem5blem2  41706  hgmapval1  41887  hdmapinvlem3  41914  hdmapinvlem4  41915  hdmapglem5  41916  hgmapvvlem1  41917  hdmapglem7b  41922  hdmapglem7  41923  lvecring  42526  prjspertr  42593  lmod0rng  48217  linc0scn0  48412  linc1  48414  lincscm  48419  lincscmcl  48421  el0ldep  48455  lindsrng01  48457  lindszr  48458  ldepsprlem  48461  ldepspr  48462  lincresunit3lem3  48463  lincresunitlem1  48464  lincresunitlem2  48465  lincresunit2  48467  lincresunit3lem1  48468