lmod0cl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lmod0cl		Structured version Visualization version GIF version

Theorem lmod0cl 20851

Description: The ring zero in a left module belongs to the set of scalars. (Contributed by NM, 11-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)

**Hypotheses**
Ref	Expression
lmod0cl.f	⊢ 𝐹 = (Scalar‘𝑊)
lmod0cl.k	⊢ 𝐾 = (Base‘𝐹)
lmod0cl.z	⊢ 0 = (0_g‘𝐹)

**Assertion**
Ref	Expression
lmod0cl	⊢ (𝑊 ∈ LMod → 0 ∈ 𝐾)

**Proof of Theorem lmod0cl**
Step	Hyp	Ref	Expression
1		lmod0cl.f	. . 3 ⊢ 𝐹 = (Scalar‘𝑊)
2	1	lmodring 20831	. 2 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)
3		lmod0cl.k	. . 3 ⊢ 𝐾 = (Base‘𝐹)
4		lmod0cl.z	. . 3 ⊢ 0 = (0_g‘𝐹)
5	3, 4	ring0cl 20214	. 2 ⊢ (𝐹 ∈ Ring → 0 ∈ 𝐾)
6	2, 5	syl 17	1 ⊢ (𝑊 ∈ LMod → 0 ∈ 𝐾)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 ‘cfv 6500 Basecbs 17148 Scalarcsca 17192 0_gc0g 17371 Ringcrg 20180 LModclmod 20823

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-sep 5243 ax-nul 5253 ax-pr 5379

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-nul 4288 df-if 4482 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-br 5101 df-opab 5163 df-mpt 5182 df-id 5527 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-iota 6456 df-fun 6502 df-fv 6508 df-riota 7325 df-ov 7371 df-0g 17373 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-grp 18878 df-ring 20182 df-lmod 20825

This theorem is referenced by: lmodfopnelem2 20862 lmodfopne 20863 lss1d 20926 lspsolvlem 21109 iporthcom 21602 lfl0f 39442 lfl1dim 39494 lfl1dim2N 39495 lkrss2N 39542 baerlem5blem1 42082 hdmap14lem2a 42240 hdmap14lem4a 42244 hdmap14lem6 42246 hgmapval0 42265 hgmapeq0 42277 lincval1 48776 lcosn0 48777 lincvalsc0 48778 lcoc0 48779 linc1 48782 lcoss 48793 el0ldep 48823

W3C validator