Theorem lmodring 20823

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ‘cfv 6493  (class class class)co 7360  Basecbs 17140  +_gcplusg 17181  ._rcmulr 17182  Scalarcsca 17184   ·_𝑠 cvsca 17185  Grpcgrp 18867  1_rcur 20120  Ringcrg 20172  LModclmod 20815

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5252

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rab 3401  df-v 3443  df-sbc 3742  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4287  df-if 4481  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-iota 6449  df-fv 6501  df-ov 7363  df-lmod 20817

This theorem is referenced by:  lmodfgrp  20824  lmodmcl  20828  lmod0cl  20843  lmod1cl  20844  lmod0vs  20850  lmodvs0  20851  lmodvsmmulgdi  20852  lmodvsneg  20861  lmodsubvs  20873  lmodsubdi  20874  lmodsubdir  20875  lssvnegcl  20911  islss3  20914  pwslmod  20925  lmodvsinv  20992  islmhm2  20994  lbsind2  21037  lspsneq  21081  lspexch  21088  ip2subdi  21603  isphld  21613  ocvlss  21631  frlmup1  21757  frlmup2  21758  frlmup3  21759  frlmup4  21760  islindf5  21798  lmisfree  21801  assasca  21821  asclghm  21842  ascl1  21845  ascldimul  21848  tlmtgp  24144  clmring  25030  lmodslmd  33267  imaslmod  33415  linds2eq  33443  lindsadd  37785  lfl0  39362  lfladd  39363  lflsub  39364  lfl0f  39366  lfladdcl  39368  lfladdcom  39369  lfladdass  39370  lfladd0l  39371  lflnegcl  39372  lflnegl  39373  lflvscl  39374  lflvsdi1  39375  lflvsdi2  39376  lflvsass  39378  lfl0sc  39379  lflsc0N  39380  lfl1sc  39381  lkrlss  39392  eqlkr  39396  eqlkr3  39398  lkrlsp  39399  ldualvsass  39438  lduallmodlem  39449  ldualvsubcl  39453  ldualvsubval  39454  lkrin  39461  dochfl1  41773  lcfl7lem  41796  lclkrlem2m  41816  lclkrlem2o  41818  lclkrlem2p  41819  lcfrlem1  41839  lcfrlem2  41840  lcfrlem3  41841  lcfrlem29  41868  lcfrlem33  41872  lcdvsubval  41915  mapdpglem30  41999  baerlem3lem1  42004  baerlem5alem1  42005  baerlem5blem1  42006  baerlem5blem2  42009  hgmapval1  42190  hdmapinvlem3  42217  hdmapinvlem4  42218  hdmapglem5  42219  hgmapvvlem1  42220  hdmapglem7b  42225  hdmapglem7  42226  lvecring  42829  prjspertr  42884  lmod0rng  48511  linc0scn0  48705  linc1  48707  lincscm  48712  lincscmcl  48714  el0ldep  48748  lindsrng01  48750  lindszr  48751  ldepsprlem  48754  ldepspr  48755  lincresunit3lem3  48756  lincresunitlem1  48757  lincresunitlem2  48758  lincresunit2  48760  lincresunit3lem1  48761