Theorem lmodring 21056

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 21052	. 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 3078  ‘cfv 6537  (class class class)co 7416  Basecbs 17305  +_gcplusg 17346  ._rcmulr 17347  Scalarcsca 17349   ·_𝑠 cvsca 17350  Grpcgrp 19061  1_rcur 20324  Ringcrg 20376  LModclmod 21048

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 2734  ax-nul 5267

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 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3079  df-rab 3415  df-v 3455  df-sbc 3743  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-iota 6493  df-fv 6545  df-ov 7419  df-lmod 21050

This theorem is used by:  lmodfgrp  21057  lmodmcl  21061  lmod0cl  21076  lmod1cl  21077  lmod0vs  21083  lmodvs0  21084  lmodvsmmulgdi  21085  lmodvsneg  21094  lmodsubvs  21106  lmodsubdi  21107  lmodsubdir  21108  lssvnegcl  21144  islss3  21147  pwslmod  21158  lmodvsinv  21224  islmhm2  21226  lbsind2  21269  lspsneq  21313  lspexch  21320  ip2subdi  21861  isphld  21871  ocvlss  21889  frlmup1  22015  frlmup2  22016  frlmup3  22017  frlmup4  22018  islindf5  22056  lmisfree  22059  assasca  22081  asclghm  22101  ascl1  22104  tlmtgp  24426  clmring  25302  lmodslmd  33646  imaslmod  33795  linds2eq  33816  lindsadd  38369  lfl0  39940  lfladd  39941  lflsub  39942  lfl0f  39944  lfladdcl  39946  lfladdcom  39947  lfladdass  39948  lfladd0l  39949  lflnegcl  39950  lflnegl  39951  lflvscl  39952  lflvsdi1  39953  lflvsdi2  39954  lflvsass  39956  lfl0sc  39957  lflsc0N  39958  lfl1sc  39959  lkrlss  39970  eqlkr  39974  eqlkr3  39976  lkrlsp  39977  ldualvsass  40016  lduallmodlem  40027  ldualvsubcl  40031  ldualvsubval  40032  lkrin  40039  dochfl1  42351  lcfl7lem  42374  lclkrlem2m  42394  lclkrlem2o  42396  lclkrlem2p  42397  lcfrlem1  42417  lcfrlem2  42418  lcfrlem3  42419  lcfrlem29  42446  lcfrlem33  42450  lcdvsubval  42493  mapdpglem30  42577  baerlem3lem1  42582  baerlem5alem1  42583  baerlem5blem1  42584  baerlem5blem2  42587  hgmapval1  42768  hdmapinvlem3  42795  hdmapinvlem4  42796  hdmapglem5  42797  hgmapvvlem1  42798  hdmapglem7b  42803  hdmapglem7  42804  lvecring  43422  prjspertr  43453  lmod0rng  49146  linc0scn0  49355  linc1  49357  lincscm  49362  lincscmcl  49364  el0ldep  49398  lindsrng01  49400  lindszr  49401  ldepsprlem  49404  ldepspr  49405  lincresunit3lem3  49406  lincresunitlem1  49407  lincresunitlem2  49408  lincresunit2  49410  lincresunit3lem1  49411