Theorem lmod0vcl 20826

Description: The zero vector is a vector. (ax-hv0cl 30985 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)

Hypotheses

Ref	Expression
0vcl.v	⊢ 𝑉 = (Base‘𝑊)
0vcl.z	⊢ 0 = (0g‘𝑊)

Assertion

Ref	Expression
lmod0vcl	⊢ (𝑊 ∈ LMod → 0 ∈ 𝑉)

Proof of Theorem lmod0vcl

Step	Hyp	Ref	Expression
1		lmodgrp 20802	. 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2		0vcl.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		0vcl.z	. . 3 ⊢ 0 = (0g‘𝑊)
4	2, 3	grpidcl 18880	. 2 ⊢ (𝑊 ∈ Grp → 0 ∈ 𝑉)
5	1, 4	syl 17	1 ⊢ (𝑊 ∈ LMod → 0 ∈ 𝑉)

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  ‘cfv 6486  Basecbs 17122  0_gc0g 17345  Grpcgrp 18848  LModclmod 20795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-iota 6442  df-fun 6488  df-fv 6494  df-riota 7309  df-ov 7355  df-0g 17347  df-mgm 18550  df-sgrp 18629  df-mnd 18645  df-grp 18851  df-lmod 20797

This theorem is referenced by:  lmodvs0  20831  lmodfopne  20835  lsssn0  20883  lspun0  20946  lsppr0  21028  lspsneq  21061  lspprat  21092  ip0r  21576  ocvlss  21611  nmhmcn  25048  lfl0  39184  lflmul  39187  lkrlss  39214  dochexmid  41587  lcfl8  41621  lcd0vcl  41733  mapdh6bN  41856  mapdh6cN  41857  hdmap1val0  41918  hdmap1l6b  41930  hdmap1l6c  41931  hdmapval0  41952  hdmaprnlem17N  41982  hdmap14lem13  41999  hdmaplkr  42032  lcoel0  48553