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 20938

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1559 ∈ wcel 2141 ‘cfv 6517 Basecbs 17228 0_gc0g 17451 Grpcgrp 18958 LModclmod 20907

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5245 ax-nul 5255 ax-pr 5389

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4480 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-br 5100 df-opab 5162 df-mpt 5181 df-id 5540 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-iota 6473 df-fun 6519 df-fv 6525 df-riota 7349 df-ov 7395 df-0g 17453 df-mgm 18657 df-sgrp 18736 df-mnd 18752 df-grp 18961 df-lmod 20909

This theorem is referenced by: lmodvs0 20943 lmodfopne 20947 lsssn0 20995 lspun0 21058 lsppr0 21139 lspsneq 21172 lspprat 21203 ip0r 21669 ocvlss 21704 nmhmcn 25162 lfl0 39653 lflmul 39656 lkrlss 39683 dochexmid 42056 lcfl8 42090 lcd0vcl 42202 mapdh6bN 42325 mapdh6cN 42326 hdmap1val0 42387 hdmap1l6b 42399 hdmap1l6c 42400 hdmapval0 42421 hdmaprnlem17N 42451 hdmap14lem13 42468 hdmaplkr 42501 lcoel0 49014