![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lmodring | Structured version Visualization version GIF version |
Description: The scalar component of a left module is a ring. (Contributed by NM, 8-Dec-2013.) (Revised by Mario Carneiro, 19-Jun-2014.) |
Ref | Expression |
---|---|
lmodring.1 | ⊢ 𝐹 = (Scalar‘𝑊) |
Ref | Expression |
---|---|
lmodring | ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2726 | . . 3 ⊢ (Base‘𝑊) = (Base‘𝑊) | |
2 | eqid 2726 | . . 3 ⊢ (+g‘𝑊) = (+g‘𝑊) | |
3 | eqid 2726 | . . 3 ⊢ ( ·𝑠 ‘𝑊) = ( ·𝑠 ‘𝑊) | |
4 | lmodring.1 | . . 3 ⊢ 𝐹 = (Scalar‘𝑊) | |
5 | eqid 2726 | . . 3 ⊢ (Base‘𝐹) = (Base‘𝐹) | |
6 | eqid 2726 | . . 3 ⊢ (+g‘𝐹) = (+g‘𝐹) | |
7 | eqid 2726 | . . 3 ⊢ (.r‘𝐹) = (.r‘𝐹) | |
8 | eqid 2726 | . . 3 ⊢ (1r‘𝐹) = (1r‘𝐹) | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | islmod 20840 | . 2 ⊢ (𝑊 ∈ LMod ↔ (𝑊 ∈ Grp ∧ 𝐹 ∈ Ring ∧ ∀𝑞 ∈ (Base‘𝐹)∀𝑟 ∈ (Base‘𝐹)∀𝑥 ∈ (Base‘𝑊)∀𝑤 ∈ (Base‘𝑊)(((𝑟( ·𝑠 ‘𝑊)𝑤) ∈ (Base‘𝑊) ∧ (𝑟( ·𝑠 ‘𝑊)(𝑤(+g‘𝑊)𝑥)) = ((𝑟( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑥)) ∧ ((𝑞(+g‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = ((𝑞( ·𝑠 ‘𝑊)𝑤)(+g‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤))) ∧ (((𝑞(.r‘𝐹)𝑟)( ·𝑠 ‘𝑊)𝑤) = (𝑞( ·𝑠 ‘𝑊)(𝑟( ·𝑠 ‘𝑊)𝑤)) ∧ ((1r‘𝐹)( ·𝑠 ‘𝑊)𝑤) = 𝑤)))) |
10 | 9 | simp2bi 1143 | 1 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 = wceq 1534 ∈ wcel 2099 ∀wral 3051 ‘cfv 6554 (class class class)co 7424 Basecbs 17213 +gcplusg 17266 .rcmulr 17267 Scalarcsca 17269 ·𝑠 cvsca 17270 Grpcgrp 18928 1rcur 20164 Ringcrg 20216 LModclmod 20836 |
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 2697 ax-nul 5311 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ne 2931 df-ral 3052 df-rab 3420 df-v 3464 df-sbc 3777 df-dif 3950 df-un 3952 df-ss 3964 df-nul 4326 df-if 4534 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-br 5154 df-iota 6506 df-fv 6562 df-ov 7427 df-lmod 20838 |
This theorem is referenced by: lmodfgrp 20845 lmodmcl 20849 lmod0cl 20864 lmod1cl 20865 lmod0vs 20871 lmodvs0 20872 lmodvsmmulgdi 20873 lmodvsneg 20882 lmodsubvs 20894 lmodsubdi 20895 lmodsubdir 20896 lssvnegcl 20933 islss3 20936 pwslmod 20947 lmodvsinv 21014 islmhm2 21016 lbsind2 21059 lspsneq 21103 lspexch 21110 ip2subdi 21640 isphld 21650 ocvlss 21668 frlmup1 21796 frlmup2 21797 frlmup3 21798 frlmup4 21799 islindf5 21837 lmisfree 21840 assasca 21860 asclghm 21880 ascl1 21882 ascldimul 21885 tlmtgp 24191 clmring 25088 lmodslmd 33068 imaslmod 33228 linds2eq 33256 lindsadd 37314 lfl0 38763 lfladd 38764 lflsub 38765 lfl0f 38767 lfladdcl 38769 lfladdcom 38770 lfladdass 38771 lfladd0l 38772 lflnegcl 38773 lflnegl 38774 lflvscl 38775 lflvsdi1 38776 lflvsdi2 38777 lflvsass 38779 lfl0sc 38780 lflsc0N 38781 lfl1sc 38782 lkrlss 38793 eqlkr 38797 eqlkr3 38799 lkrlsp 38800 ldualvsass 38839 lduallmodlem 38850 ldualvsubcl 38854 ldualvsubval 38855 lkrin 38862 dochfl1 41175 lcfl7lem 41198 lclkrlem2m 41218 lclkrlem2o 41220 lclkrlem2p 41221 lcfrlem1 41241 lcfrlem2 41242 lcfrlem3 41243 lcfrlem29 41270 lcfrlem33 41274 lcdvsubval 41317 mapdpglem30 41401 baerlem3lem1 41406 baerlem5alem1 41407 baerlem5blem1 41408 baerlem5blem2 41411 hgmapval1 41592 hdmapinvlem3 41619 hdmapinvlem4 41620 hdmapglem5 41621 hgmapvvlem1 41622 hdmapglem7b 41627 hdmapglem7 41628 lvecring 42010 prjspertr 42259 lmod0rng 47606 linc0scn0 47806 linc1 47808 lincscm 47813 lincscmcl 47815 el0ldep 47849 lindsrng01 47851 lindszr 47852 ldepsprlem 47855 ldepspr 47856 lincresunit3lem3 47857 lincresunitlem1 47858 lincresunitlem2 47859 lincresunit2 47861 lincresunit3lem1 47862 |
Copyright terms: Public domain | W3C validator |