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 21049

Description: The zero vector is a vector. (ax-hv0cl 31392 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 21025	. 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2		0vcl.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		0vcl.z	. . 3 ⊢ 0 = (0_g‘𝑊)
4	2, 3	grpidcl 19063	. 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 1570 ∈ wcel 2146 ‘cfv 6543 Basecbs 17294 0_gc0g 17517 Grpcgrp 19031 LModclmod 21018

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-sep 5262 ax-nul 5274 ax-pr 5409

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-ral 3083 df-rex 3093 df-rmo 3372 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-br 5115 df-opab 5179 df-mpt 5198 df-id 5561 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-iota 6499 df-fun 6545 df-fv 6551 df-riota 7380 df-ov 7426 df-0g 17519 df-mgm 18723 df-sgrp 18806 df-mnd 18822 df-grp 19034 df-lmod 21020

This theorem is used by: lmodvs0 21054 lmodfopne 21058 lsssn0 21106 lspun0 21169 lsppr0 21250 lspsneq 21283 lspprat 21314 ip0r 21824 ocvlss 21859 nmhmcn 25316 lfl0 39880 lflmul 39883 lkrlss 39910 dochexmid 42283 lcfl8 42317 lcd0vcl 42429 mapdh6bN 42552 mapdh6cN 42553 hdmap1val0 42614 hdmap1l6b 42626 hdmap1l6c 42627 hdmapval0 42648 hdmaprnlem17N 42678 hdmap14lem13 42695 hdmaplkr 42728 lcoel0 49249