Theorem lmodring 18694

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ‘cfv 5804  (class class class)co 6549  Basecbs 15695  +_gcplusg 15768  ._rcmulr 15769  Scalarcsca 15771   ·_𝑠 cvsca 15772  Grpcgrp 17245  1_rcur 18324  Ringcrg 18370  LModclmod 18686

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-lmod 18688

This theorem is referenced by:  lmodfgrp  18695  lmodmcl  18698  lmod0cl  18712  lmod1cl  18713  lmod0vs  18719  lmodvs0  18720  lmodvsmmulgdi  18721  lmodvsneg  18730  lmodsubvs  18742  lmodsubdi  18743  lmodsubdir  18744  lssvnegcl  18777  islss3  18780  pwslmod  18791  lmodvsinv  18857  islmhm2  18859  lbsind2  18902  lspsneq  18943  lspexch  18950  asclghm  19159  ip2subdi  19808  isphld  19818  ocvlss  19835  frlmup1  19956  frlmup2  19957  frlmup3  19958  frlmup4  19959  islindf5  19997  lmisfree  20000  tlmtgp  21809  clmring  22678  lmodslmd  29088  lfl0  33370  lfladd  33371  lflsub  33372  lfl0f  33374  lfladdcl  33376  lfladdcom  33377  lfladdass  33378  lfladd0l  33379  lflnegcl  33380  lflnegl  33381  lflvscl  33382  lflvsdi1  33383  lflvsdi2  33384  lflvsass  33386  lfl0sc  33387  lflsc0N  33388  lfl1sc  33389  lkrlss  33400  eqlkr  33404  eqlkr3  33406  lkrlsp  33407  ldualvsass  33446  lduallmodlem  33457  ldualvsubcl  33461  ldualvsubval  33462  lkrin  33469  dochfl1  35783  lcfl7lem  35806  lclkrlem2m  35826  lclkrlem2o  35828  lclkrlem2p  35829  lcfrlem1  35849  lcfrlem2  35850  lcfrlem3  35851  lcfrlem29  35878  lcfrlem33  35882  lcdvsubval  35925  mapdpglem30  36009  baerlem3lem1  36014  baerlem5alem1  36015  baerlem5blem1  36016  baerlem5blem2  36019  hgmapval1  36203  hdmapinvlem3  36230  hdmapinvlem4  36231  hdmapglem5  36232  hgmapvvlem1  36233  hdmapglem7b  36238  hdmapglem7  36239  lmod0rng  41658  ascl1  41960  linc0scn0  42006  linc1  42008  lincscm  42013  lincscmcl  42015  el0ldep  42049  lindsrng01  42051  lindszr  42052  ldepsprlem  42055  ldepspr  42056  lincresunit3lem3  42057  lincresunitlem1  42058  lincresunitlem2  42059  lincresunit2  42061  lincresunit3lem1  42062