Theorem lmodring 19263

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071   = wceq 1601   ∈ wcel 2107  ∀wral 3090  ‘cfv 6135  (class class class)co 6922  Basecbs 16255  +_gcplusg 16338  ._rcmulr 16339  Scalarcsca 16341   ·_𝑠 cvsca 16342  Grpcgrp 17809  1_rcur 18888  Ringcrg 18934  LModclmod 19255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-nul 5025

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925  df-lmod 19257

This theorem is referenced by:  lmodfgrp  19264  lmodmcl  19267  lmod0cl  19281  lmod1cl  19282  lmod0vs  19288  lmodvs0  19289  lmodvsmmulgdi  19290  lmodvsneg  19299  lmodsubvs  19311  lmodsubdi  19312  lmodsubdir  19313  lssvnegcl  19351  islss3  19354  pwslmod  19365  lmodvsinv  19431  islmhm2  19433  lbsind2  19476  lspsneq  19517  lspexch  19525  asclghm  19735  ip2subdi  20387  isphld  20397  ocvlss  20415  frlmup1  20541  frlmup2  20542  frlmup3  20543  frlmup4  20544  islindf5  20582  lmisfree  20585  tlmtgp  22407  clmring  23277  lmodslmd  30319  imaslmod  30411  lindsadd  34030  lfl0  35221  lfladd  35222  lflsub  35223  lfl0f  35225  lfladdcl  35227  lfladdcom  35228  lfladdass  35229  lfladd0l  35230  lflnegcl  35231  lflnegl  35232  lflvscl  35233  lflvsdi1  35234  lflvsdi2  35235  lflvsass  35237  lfl0sc  35238  lflsc0N  35239  lfl1sc  35240  lkrlss  35251  eqlkr  35255  eqlkr3  35257  lkrlsp  35258  ldualvsass  35297  lduallmodlem  35308  ldualvsubcl  35312  ldualvsubval  35313  lkrin  35320  dochfl1  37632  lcfl7lem  37655  lclkrlem2m  37675  lclkrlem2o  37677  lclkrlem2p  37678  lcfrlem1  37698  lcfrlem2  37699  lcfrlem3  37700  lcfrlem29  37727  lcfrlem33  37731  lcdvsubval  37774  mapdpglem30  37858  baerlem3lem1  37863  baerlem5alem1  37864  baerlem5blem1  37865  baerlem5blem2  37868  hgmapval1  38049  hdmapinvlem3  38076  hdmapinvlem4  38077  hdmapglem5  38078  hgmapvvlem1  38079  hdmapglem7b  38084  hdmapglem7  38085  lvecring  38137  prjspertr  38208  lmod0rng  42887  ascl1  43185  linc0scn0  43231  linc1  43233  lincscm  43238  lincscmcl  43240  el0ldep  43274  lindsrng01  43276  lindszr  43277  ldepsprlem  43280  ldepspr  43281  lincresunit3lem3  43282  lincresunitlem1  43283  lincresunitlem2  43284  lincresunit2  43286  lincresunit3lem1  43287