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 20888

Description: The zero vector is a vector. (ax-hv0cl 31099 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 20864	. 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2		0vcl.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		0vcl.z	. . 3 ⊢ 0 = (0_g‘𝑊)
4	2, 3	grpidcl 18939	. 2 ⊢ (𝑊 ∈ Grp → 0 ∈ 𝑉)
5	1, 4	syl 17	1 ⊢ (𝑊 ∈ LMod → 0 ∈ 𝑉)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1547 ∈ wcel 2119 ‘cfv 6492 Basecbs 17177 0_gc0g 17400 Grpcgrp 18907 LModclmod 20857

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-sep 5225 ax-nul 5235 ax-pr 5369

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-ral 3055 df-rex 3065 df-rmo 3345 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4269 df-if 4462 df-sn 4563 df-pr 4565 df-op 4569 df-uni 4846 df-br 5080 df-opab 5142 df-mpt 5161 df-id 5520 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-iota 6448 df-fun 6494 df-fv 6500 df-riota 7320 df-ov 7366 df-0g 17402 df-mgm 18606 df-sgrp 18685 df-mnd 18701 df-grp 18910 df-lmod 20859

This theorem is referenced by: lmodvs0 20893 lmodfopne 20897 lsssn0 20945 lspun0 21008 lsppr0 21089 lspsneq 21122 lspprat 21153 ip0r 21619 ocvlss 21654 nmhmcn 25112 lfl0 39564 lflmul 39567 lkrlss 39594 dochexmid 41967 lcfl8 42001 lcd0vcl 42113 mapdh6bN 42236 mapdh6cN 42237 hdmap1val0 42298 hdmap1l6b 42310 hdmap1l6c 42311 hdmapval0 42332 hdmaprnlem17N 42362 hdmap14lem13 42379 hdmaplkr 42412 lcoel0 48926