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

Theorem lmod0cl 19098
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
StepHypRef Expression
1 lmod0cl.f . . 3 𝐹 = (Scalar‘𝑊)
21lmodring 19080 . 2 (𝑊 ∈ LMod → 𝐹 ∈ Ring)
3 lmod0cl.k . . 3 𝐾 = (Base‘𝐹)
4 lmod0cl.z . . 3 0 = (0g𝐹)
53, 4ring0cl 18776 . 2 (𝐹 ∈ Ring → 0𝐾)
62, 5syl 17 1 (𝑊 ∈ LMod → 0𝐾)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  wcel 2144  cfv 6031  Basecbs 16063  Scalarcsca 16151  0gc0g 16307  Ringcrg 18754  LModclmod 19072
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-nul 4062  df-if 4224  df-sn 4315  df-pr 4317  df-op 4321  df-uni 4573  df-br 4785  df-opab 4845  df-mpt 4862  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-iota 5994  df-fun 6033  df-fv 6039  df-riota 6753  df-ov 6795  df-0g 16309  df-mgm 17449  df-sgrp 17491  df-mnd 17502  df-grp 17632  df-ring 18756  df-lmod 19074
This theorem is referenced by:  lmodfopnelem2  19109  lmodfopne  19110  lss1d  19175  lspsolvlem  19355  iporthcom  20196  lfl0f  34871  lfl1dim  34923  lfl1dim2N  34924  lkrss2N  34971  baerlem5blem1  37512  hdmap14lem2a  37670  hdmap14lem4a  37674  hdmap14lem6  37676  hgmapval0  37695  hgmapeq0  37707  lincval1  42726  lcosn0  42727  lincvalsc0  42728  lcoc0  42729  linc1  42732  lcoss  42743  el0ldep  42773
  Copyright terms: Public domain W3C validator