Theorem lmodring 19073

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 19069	. 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ (Base‘𝐹)∀𝑟 ∈ (Base‘𝐹)∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠 ‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑥)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = ((𝑞( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = (𝑞( ·𝑠 ‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤)) ∧ ((1r‘𝐹)( ·𝑠 ‘𝑊)𝑤) = 𝑤))))
10	9	simp2bi 1141	1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139  ∀wral 3050  ‘cfv 6049  (class class class)co 6813  Basecbs 16059  +_gcplusg 16143  ._rcmulr 16144  Scalarcsca 16146   ·_𝑠 cvsca 16147  Grpcgrp 17623  1_rcur 18701  Ringcrg 18747  LModclmod 19065

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-nul 4941

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816  df-lmod 19067

This theorem is referenced by:  lmodfgrp  19074  lmodmcl  19077  lmod0cl  19091  lmod1cl  19092  lmod0vs  19098  lmodvs0  19099  lmodvsmmulgdi  19100  lmodvsneg  19109  lmodsubvs  19121  lmodsubdi  19122  lmodsubdir  19123  lssvnegcl  19158  islss3  19161  pwslmod  19172  lmodvsinv  19238  islmhm2  19240  lbsind2  19283  lspsneq  19324  lspexch  19331  asclghm  19540  ip2subdi  20191  isphld  20201  ocvlss  20218  frlmup1  20339  frlmup2  20340  frlmup3  20341  frlmup4  20342  islindf5  20380  lmisfree  20383  tlmtgp  22200  clmring  23070  lmodslmd  30066  lfl0  34855  lfladd  34856  lflsub  34857  lfl0f  34859  lfladdcl  34861  lfladdcom  34862  lfladdass  34863  lfladd0l  34864  lflnegcl  34865  lflnegl  34866  lflvscl  34867  lflvsdi1  34868  lflvsdi2  34869  lflvsass  34871  lfl0sc  34872  lflsc0N  34873  lfl1sc  34874  lkrlss  34885  eqlkr  34889  eqlkr3  34891  lkrlsp  34892  ldualvsass  34931  lduallmodlem  34942  ldualvsubcl  34946  ldualvsubval  34947  lkrin  34954  dochfl1  37267  lcfl7lem  37290  lclkrlem2m  37310  lclkrlem2o  37312  lclkrlem2p  37313  lcfrlem1  37333  lcfrlem2  37334  lcfrlem3  37335  lcfrlem29  37362  lcfrlem33  37366  lcdvsubval  37409  mapdpglem30  37493  baerlem3lem1  37498  baerlem5alem1  37499  baerlem5blem1  37500  baerlem5blem2  37503  hgmapval1  37687  hdmapinvlem3  37714  hdmapinvlem4  37715  hdmapglem5  37716  hgmapvvlem1  37717  hdmapglem7b  37722  hdmapglem7  37723  lmod0rng  42378  ascl1  42676  linc0scn0  42722  linc1  42724  lincscm  42729  lincscmcl  42731  el0ldep  42765  lindsrng01  42767  lindszr  42768  ldepsprlem  42771  ldepspr  42772  lincresunit3lem3  42773  lincresunitlem1  42774  lincresunitlem2  42775  lincresunit2  42777  lincresunit3lem1  42778