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 20874

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 20854	. 2 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)
3		lmod0cl.k	. . 3 ⊢ 𝐾 = (Base‘𝐹)
4		lmod0cl.z	. . 3 ⊢ 0 = (0_g‘𝐹)
5	3, 4	ring0cl 20239	. 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 6492 Basecbs 17170 Scalarcsca 17214 0_gc0g 17393 Ringcrg 20205 LModclmod 20846

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 5231 ax-nul 5241 ax-pr 5370

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 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-iota 6448 df-fun 6494 df-fv 6500 df-riota 7317 df-ov 7363 df-0g 17395 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-grp 18903 df-ring 20207 df-lmod 20848

This theorem is referenced by: lmodfopnelem2 20885 lmodfopne 20886 lss1d 20949 lspsolvlem 21132 iporthcom 21625 lfl0f 39529 lfl1dim 39581 lfl1dim2N 39582 lkrss2N 39629 baerlem5blem1 42169 hdmap14lem2a 42327 hdmap14lem4a 42331 hdmap14lem6 42333 hgmapval0 42352 hgmapeq0 42364 lincval1 48907 lcosn0 48908 lincvalsc0 48909 lcoc0 48910 linc1 48913 lcoss 48924 el0ldep 48954

W3C validator