![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lmod0cl | Structured version Visualization version GIF version |
Description: The ring zero in a left module belongs to the ring base set. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
Ref | Expression |
---|---|
lmod0cl.f | ⊢ 𝐹 = (Scalar‘𝑊) |
lmod0cl.k | ⊢ 𝐾 = (Base‘𝐹) |
lmod0cl.z | ⊢ 0 = (0g‘𝐹) |
Ref | Expression |
---|---|
lmod0cl | ⊢ (𝑊 ∈ LMod → 0 ∈ 𝐾) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmod0cl.f | . . 3 ⊢ 𝐹 = (Scalar‘𝑊) | |
2 | 1 | lmodring 19376 | . 2 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring) |
3 | lmod0cl.k | . . 3 ⊢ 𝐾 = (Base‘𝐹) | |
4 | lmod0cl.z | . . 3 ⊢ 0 = (0g‘𝐹) | |
5 | 3, 4 | ring0cl 19054 | . 2 ⊢ (𝐹 ∈ Ring → 0 ∈ 𝐾) |
6 | 2, 5 | syl 17 | 1 ⊢ (𝑊 ∈ LMod → 0 ∈ 𝐾) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1507 ∈ wcel 2050 ‘cfv 6185 Basecbs 16337 Scalarcsca 16422 0gc0g 16567 Ringcrg 19032 LModclmod 19368 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-sep 5056 ax-nul 5063 ax-pow 5115 ax-pr 5182 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-ral 3087 df-rex 3088 df-reu 3089 df-rmo 3090 df-rab 3091 df-v 3411 df-sbc 3676 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-nul 4173 df-if 4345 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4709 df-br 4926 df-opab 4988 df-mpt 5005 df-id 5308 df-xp 5409 df-rel 5410 df-cnv 5411 df-co 5412 df-dm 5413 df-iota 6149 df-fun 6187 df-fv 6193 df-riota 6935 df-ov 6977 df-0g 16569 df-mgm 17722 df-sgrp 17764 df-mnd 17775 df-grp 17906 df-ring 19034 df-lmod 19370 |
This theorem is referenced by: lmodfopnelem2 19405 lmodfopne 19406 lss1d 19469 lspsolvlem 19648 iporthcom 20493 lfl0f 35679 lfl1dim 35731 lfl1dim2N 35732 lkrss2N 35779 baerlem5blem1 38319 hdmap14lem2a 38477 hdmap14lem4a 38481 hdmap14lem6 38483 hgmapval0 38502 hgmapeq0 38514 lincval1 43866 lcosn0 43867 lincvalsc0 43868 lcoc0 43869 linc1 43872 lcoss 43883 el0ldep 43913 |
Copyright terms: Public domain | W3C validator |