Theorem lmodring 20745

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  ∀wral 3057  ‘cfv 6543  (class class class)co 7415  Basecbs 17174  +_gcplusg 17227  ._rcmulr 17228  Scalarcsca 17230   ·_𝑠 cvsca 17231  Grpcgrp 18884  1_rcur 20115  Ringcrg 20167  LModclmod 20737

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5301

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2937  df-ral 3058  df-rab 3429  df-v 3472  df-sbc 3776  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-br 5144  df-iota 6495  df-fv 6551  df-ov 7418  df-lmod 20739

This theorem is referenced by:  lmodfgrp  20746  lmodmcl  20750  lmod0cl  20765  lmod1cl  20766  lmod0vs  20772  lmodvs0  20773  lmodvsmmulgdi  20774  lmodvsneg  20783  lmodsubvs  20795  lmodsubdi  20796  lmodsubdir  20797  lssvnegcl  20834  islss3  20837  pwslmod  20848  lmodvsinv  20915  islmhm2  20917  lbsind2  20960  lspsneq  21004  lspexch  21011  ip2subdi  21570  isphld  21580  ocvlss  21598  frlmup1  21726  frlmup2  21727  frlmup3  21728  frlmup4  21729  islindf5  21767  lmisfree  21770  assasca  21790  asclghm  21810  ascl1  21812  ascldimul  21815  tlmtgp  24094  clmring  24991  lmodslmd  32906  imaslmod  33060  linds2eq  33091  lindsadd  37081  lfl0  38532  lfladd  38533  lflsub  38534  lfl0f  38536  lfladdcl  38538  lfladdcom  38539  lfladdass  38540  lfladd0l  38541  lflnegcl  38542  lflnegl  38543  lflvscl  38544  lflvsdi1  38545  lflvsdi2  38546  lflvsass  38548  lfl0sc  38549  lflsc0N  38550  lfl1sc  38551  lkrlss  38562  eqlkr  38566  eqlkr3  38568  lkrlsp  38569  ldualvsass  38608  lduallmodlem  38619  ldualvsubcl  38623  ldualvsubval  38624  lkrin  38631  dochfl1  40944  lcfl7lem  40967  lclkrlem2m  40987  lclkrlem2o  40989  lclkrlem2p  40990  lcfrlem1  41010  lcfrlem2  41011  lcfrlem3  41012  lcfrlem29  41039  lcfrlem33  41043  lcdvsubval  41086  mapdpglem30  41170  baerlem3lem1  41175  baerlem5alem1  41176  baerlem5blem1  41177  baerlem5blem2  41180  hgmapval1  41361  hdmapinvlem3  41388  hdmapinvlem4  41389  hdmapglem5  41390  hgmapvvlem1  41391  hdmapglem7b  41396  hdmapglem7  41397  lvecring  41759  prjspertr  42020  lmod0rng  47282  linc0scn0  47482  linc1  47484  lincscm  47489  lincscmcl  47491  el0ldep  47525  lindsrng01  47527  lindszr  47528  ldepsprlem  47531  ldepspr  47532  lincresunit3lem3  47533  lincresunitlem1  47534  lincresunitlem2  47535  lincresunit2  47537  lincresunit3lem1  47538