lmod0vcl - Metamath Proof Explorer

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

Theorem lmod0vcl 21172

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

**Hypotheses**
Ref	Expression
0vcl.v	⊢ 𝑉 = (Base‘𝑊)
0vcl.z	⊢ 0 = (0_g‘𝑊)

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

**Proof of Theorem lmod0vcl**
Step	Hyp	Ref	Expression
1		lmodgrp 21148	. 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2		0vcl.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		0vcl.z	. . 3 ⊢ 0 = (0_g‘𝑊)
4	2, 3	grpidcl 19182	. 2 ⊢ (𝑊 ∈ Grp → 0 ∈ 𝑉)
5	1, 4	syl 18	1 ⊢ (𝑊 ∈ LMod → 0 ∈ 𝑉)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 = wceq 1569 ∈ wcel 2144 ‘cfv 6539 Basecbs 17393 0_gc0g 17616 Grpcgrp 19150 LModclmod 21141

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pr 5390

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-ss 3896 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-br 5103 df-opab 5167 df-mpt 5186 df-id 5545 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-iota 6494 df-fun 6541 df-fv 6547 df-riota 7378 df-ov 7424 df-0g 17618 df-mgm 18822 df-sgrp 18914 df-mnd 18930 df-grp 19153 df-lmod 21143

This theorem is used by: lmodvs0 21177 lmodfopne 21181 lsssn0 21229 lspun0 21292 lsppr0 21373 lspsneq 21406 lspprat 21437 ip0r 21949 ocvlss 21984 nmhmcn 25447 lfl0 40216 lflmul 40219 lkrlss 40246 dochexmid 42619 lcfl8 42653 lcd0vcl 42765 mapdh6bN 42888 mapdh6cN 42889 hdmap1val0 42950 hdmap1l6b 42962 hdmap1l6c 42963 hdmapval0 42984 hdmaprnlem17N 43014 hdmap14lem13 43031 hdmaplkr 43064 lcoel0 49634