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 21199

Description: The zero vector is a vector. (ax-hv0cl 31638 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 21175	. 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2		0vcl.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		0vcl.z	. . 3 ⊢ 0 = (0_g‘𝑊)
4	2, 3	grpidcl 19208	. 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 2147 ‘cfv 6561 Basecbs 17419 0_gc0g 17642 Grpcgrp 19176 LModclmod 21168

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-sep 5253 ax-nul 5264 ax-pr 5396

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-ss 3901 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-br 5107 df-opab 5172 df-mpt 5191 df-id 5551 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-iota 6515 df-fun 6563 df-fv 6569 df-riota 7403 df-ov 7449 df-0g 17644 df-mgm 18848 df-sgrp 18940 df-mnd 18956 df-grp 19179 df-lmod 21170

This theorem is used by: lmodvs0 21204 lmodfopne 21208 lsssn0 21256 lspun0 21319 lsppr0 21400 lspsneq 21433 lspprat 21464 ip0r 21976 ocvlss 22011 nmhmcn 25474 lfl0 40325 lflmul 40328 lkrlss 40355 dochexmid 42728 lcfl8 42762 lcd0vcl 42874 mapdh6bN 42997 mapdh6cN 42998 hdmap1val0 43059 hdmap1l6b 43071 hdmap1l6c 43072 hdmapval0 43093 hdmaprnlem17N 43123 hdmap14lem13 43140 hdmaplkr 43173 lcoel0 49755