![]() |
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 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) |
Colors of variables: wff setvar class |
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 1rcur 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 |
Copyright terms: Public domain | W3C validator |