Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > lmodring | Structured version Visualization version Unicode 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2622 | . . 3 | |
2 | eqid 2622 | . . 3 | |
3 | eqid 2622 | . . 3 | |
4 | lmodring.1 | . . 3 Scalar | |
5 | eqid 2622 | . . 3 | |
6 | eqid 2622 | . . 3 | |
7 | eqid 2622 | . . 3 | |
8 | eqid 2622 | . . 3 | |
9 | 1, 2, 3, 4, 5, 6, 7, 8 | islmod 18867 | . 2 |
10 | 9 | simp2bi 1077 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 wceq 1483 wcel 1990 wral 2912 cfv 5888 (class class class)co 6650 cbs 15857 cplusg 15941 cmulr 15942 Scalarcsca 15944 cvsca 15945 cgrp 17422 cur 18501 crg 18547 clmod 18863 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-nul 4789 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-iota 5851 df-fv 5896 df-ov 6653 df-lmod 18865 |
This theorem is referenced by: lmodfgrp 18872 lmodmcl 18875 lmod0cl 18889 lmod1cl 18890 lmod0vs 18896 lmodvs0 18897 lmodvsmmulgdi 18898 lmodvsneg 18907 lmodsubvs 18919 lmodsubdi 18920 lmodsubdir 18921 lssvnegcl 18956 islss3 18959 pwslmod 18970 lmodvsinv 19036 islmhm2 19038 lbsind2 19081 lspsneq 19122 lspexch 19129 asclghm 19338 ip2subdi 19989 isphld 19999 ocvlss 20016 frlmup1 20137 frlmup2 20138 frlmup3 20139 frlmup4 20140 islindf5 20178 lmisfree 20181 tlmtgp 21999 clmring 22870 lmodslmd 29757 lfl0 34352 lfladd 34353 lflsub 34354 lfl0f 34356 lfladdcl 34358 lfladdcom 34359 lfladdass 34360 lfladd0l 34361 lflnegcl 34362 lflnegl 34363 lflvscl 34364 lflvsdi1 34365 lflvsdi2 34366 lflvsass 34368 lfl0sc 34369 lflsc0N 34370 lfl1sc 34371 lkrlss 34382 eqlkr 34386 eqlkr3 34388 lkrlsp 34389 ldualvsass 34428 lduallmodlem 34439 ldualvsubcl 34443 ldualvsubval 34444 lkrin 34451 dochfl1 36765 lcfl7lem 36788 lclkrlem2m 36808 lclkrlem2o 36810 lclkrlem2p 36811 lcfrlem1 36831 lcfrlem2 36832 lcfrlem3 36833 lcfrlem29 36860 lcfrlem33 36864 lcdvsubval 36907 mapdpglem30 36991 baerlem3lem1 36996 baerlem5alem1 36997 baerlem5blem1 36998 baerlem5blem2 37001 hgmapval1 37185 hdmapinvlem3 37212 hdmapinvlem4 37213 hdmapglem5 37214 hgmapvvlem1 37215 hdmapglem7b 37220 hdmapglem7 37221 lmod0rng 41868 ascl1 42166 linc0scn0 42212 linc1 42214 lincscm 42219 lincscmcl 42221 el0ldep 42255 lindsrng01 42257 lindszr 42258 ldepsprlem 42261 ldepspr 42262 lincresunit3lem3 42263 lincresunitlem1 42264 lincresunitlem2 42265 lincresunit2 42267 lincresunit3lem1 42268 |
Copyright terms: Public domain | W3C validator |