![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > lmod0vcl | Structured version Visualization version GIF version |
Description: The zero vector is a vector. (ax-hv0cl 28414 analog.) (Contributed by NM, 10-Jan-2014.) (Revised by Mario Carneiro, 19-Jun-2014.) |
Ref | Expression |
---|---|
0vcl.v | ⊢ 𝑉 = (Base‘𝑊) |
0vcl.z | ⊢ 0 = (0g‘𝑊) |
Ref | Expression |
---|---|
lmod0vcl | ⊢ (𝑊 ∈ LMod → 0 ∈ 𝑉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lmodgrp 19225 | . 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | |
2 | 0vcl.v | . . 3 ⊢ 𝑉 = (Base‘𝑊) | |
3 | 0vcl.z | . . 3 ⊢ 0 = (0g‘𝑊) | |
4 | 2, 3 | grpidcl 17803 | . 2 ⊢ (𝑊 ∈ Grp → 0 ∈ 𝑉) |
5 | 1, 4 | syl 17 | 1 ⊢ (𝑊 ∈ LMod → 0 ∈ 𝑉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1658 ∈ wcel 2166 ‘cfv 6122 Basecbs 16221 0gc0g 16452 Grpcgrp 17775 LModclmod 19218 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-8 2168 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 ax-sep 5004 ax-nul 5012 ax-pow 5064 ax-pr 5126 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ne 2999 df-ral 3121 df-rex 3122 df-reu 3123 df-rmo 3124 df-rab 3125 df-v 3415 df-sbc 3662 df-dif 3800 df-un 3802 df-in 3804 df-ss 3811 df-nul 4144 df-if 4306 df-sn 4397 df-pr 4399 df-op 4403 df-uni 4658 df-br 4873 df-opab 4935 df-mpt 4952 df-id 5249 df-xp 5347 df-rel 5348 df-cnv 5349 df-co 5350 df-dm 5351 df-iota 6085 df-fun 6124 df-fv 6130 df-riota 6865 df-ov 6907 df-0g 16454 df-mgm 17594 df-sgrp 17636 df-mnd 17647 df-grp 17778 df-lmod 19220 |
This theorem is referenced by: lmodvs0 19252 lmodfopne 19256 lsssn0 19303 lspun0 19369 lsppr0 19450 lspsneq 19480 lspprat 19513 ip0r 20343 ocvlss 20378 nmhmcn 23288 lfl0 35139 lflmul 35142 lkrlss 35169 dochexmid 37542 lcfl8 37576 lcd0vcl 37688 mapdh6bN 37811 mapdh6cN 37812 hdmap1val0 37873 hdmap1l6b 37885 hdmap1l6c 37886 hdmapval0 37907 hdmaprnlem17N 37937 hdmap14lem13 37954 hdmaplkr 37987 lcoel0 43063 |
Copyright terms: Public domain | W3C validator |