Theorem lmod0cl 19394

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.)

Hypotheses

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

Assertion

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

Proof of Theorem lmod0cl

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 ∈ 𝐾)

Syntax hints:   → wi 4   = wceq 1507   ∈ wcel 2050  ‘cfv 6185  Basecbs 16337  Scalarcsca 16422  0_gc0g 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