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 21081

Description: The zero vector is a vector. (ax-hv0cl 31492 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 21057	. 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2		0vcl.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		0vcl.z	. . 3 ⊢ 0 = (0_g‘𝑊)
4	2, 3	grpidcl 19095	. 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 2145 ‘cfv 6537 Basecbs 17307 0_gc0g 17530 Grpcgrp 19063 LModclmod 21050

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 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2734 ax-sep 5255 ax-nul 5267 ax-pr 5402

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 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-ral 3079 df-rex 3089 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3455 df-sbc 3743 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4283 df-if 4486 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4871 df-br 5108 df-opab 5172 df-mpt 5191 df-id 5554 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-iota 6493 df-fun 6539 df-fv 6545 df-riota 7374 df-ov 7420 df-0g 17532 df-mgm 18736 df-sgrp 18827 df-mnd 18843 df-grp 19066 df-lmod 21052

This theorem is used by: lmodvs0 21086 lmodfopne 21090 lsssn0 21138 lspun0 21201 lsppr0 21282 lspsneq 21315 lspprat 21346 ip0r 21856 ocvlss 21891 nmhmcn 25354 lfl0 39946 lflmul 39949 lkrlss 39976 dochexmid 42349 lcfl8 42383 lcd0vcl 42495 mapdh6bN 42618 mapdh6cN 42619 hdmap1val0 42680 hdmap1l6b 42692 hdmap1l6c 42693 hdmapval0 42714 hdmaprnlem17N 42744 hdmap14lem13 42761 hdmaplkr 42794 lcoel0 49366