Theorem lmodring 21000

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102   = wceq 1569   ∈ wcel 2142  ∀wral 3078  ‘cfv 6536  (class class class)co 7412  Basecbs 17275  +_gcplusg 17316  ._rcmulr 17317  Scalarcsca 17319   ·_𝑠 cvsca 17320  Grpcgrp 19006  1_rcur 20269  Ringcrg 20321  LModclmod 20992

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5268

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3416  df-v 3456  df-sbc 3744  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-iota 6492  df-fv 6544  df-ov 7415  df-lmod 20994

This theorem is used by:  lmodfgrp  21001  lmodmcl  21005  lmod0cl  21020  lmod1cl  21021  lmod0vs  21027  lmodvs0  21028  lmodvsmmulgdi  21029  lmodvsneg  21038  lmodsubvs  21050  lmodsubdi  21051  lmodsubdir  21052  lssvnegcl  21088  islss3  21091  pwslmod  21102  lmodvsinv  21168  islmhm2  21170  lbsind2  21213  lspsneq  21257  lspexch  21264  ip2subdi  21805  isphld  21815  ocvlss  21833  frlmup1  21959  frlmup2  21960  frlmup3  21961  frlmup4  21962  islindf5  22000  lmisfree  22003  assasca  22023  asclghm  22043  ascl1  22046  tlmtgp  24364  clmring  25240  lmodslmd  33533  imaslmod  33682  linds2eq  33703  lindsadd  38292  lfl0  39867  lfladd  39868  lflsub  39869  lfl0f  39871  lfladdcl  39873  lfladdcom  39874  lfladdass  39875  lfladd0l  39876  lflnegcl  39877  lflnegl  39878  lflvscl  39879  lflvsdi1  39880  lflvsdi2  39881  lflvsass  39883  lfl0sc  39884  lflsc0N  39885  lfl1sc  39886  lkrlss  39897  eqlkr  39901  eqlkr3  39903  lkrlsp  39904  ldualvsass  39943  lduallmodlem  39954  ldualvsubcl  39958  ldualvsubval  39959  lkrin  39966  dochfl1  42278  lcfl7lem  42301  lclkrlem2m  42321  lclkrlem2o  42323  lclkrlem2p  42324  lcfrlem1  42344  lcfrlem2  42345  lcfrlem3  42346  lcfrlem29  42373  lcfrlem33  42377  lcdvsubval  42420  mapdpglem30  42504  baerlem3lem1  42509  baerlem5alem1  42510  baerlem5blem1  42511  baerlem5blem2  42514  hgmapval1  42695  hdmapinvlem3  42722  hdmapinvlem4  42723  hdmapglem5  42724  hgmapvvlem1  42725  hdmapglem7b  42730  hdmapglem7  42731  lvecring  43334  prjspertr  43365  lmod0rng  49022  linc0scn0  49231  linc1  49233  lincscm  49238  lincscmcl  49240  el0ldep  49274  lindsrng01  49276  lindszr  49277  ldepsprlem  49280  ldepspr  49281  lincresunit3lem3  49282  lincresunitlem1  49283  lincresunitlem2  49284  lincresunit2  49286  lincresunit3lem1  49287