| 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 31264 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 20957 | . 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp) | |
| 2 | 0vcl.v | . . 3 ⊢ 𝑉 = (Base‘𝑊) | |
| 3 | 0vcl.z | . . 3 ⊢ 0 = (0g‘𝑊) | |
| 4 | 2, 3 | grpidcl 19022 | . 2 ⊢ (𝑊 ∈ Grp → 0 ∈ 𝑉) |
| 5 | 1, 4 | syl 18 | 1 ⊢ (𝑊 ∈ LMod → 0 ∈ 𝑉) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1563 ∈ wcel 2145 ‘cfv 6525 Basecbs 17259 0gc0g 17482 Grpcgrp 18990 LModclmod 20950 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pr 5395 |
| This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-br 5106 df-opab 5168 df-mpt 5187 df-id 5547 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-iota 6481 df-fun 6527 df-fv 6533 df-riota 7357 df-ov 7403 df-0g 17484 df-mgm 18688 df-sgrp 18767 df-mnd 18783 df-grp 18993 df-lmod 20952 |
| This theorem is referenced by: lmodvs0 20986 lmodfopne 20990 lsssn0 21038 lspun0 21101 lsppr0 21182 lspsneq 21215 lspprat 21246 ip0r 21747 ocvlss 21782 nmhmcn 25240 lfl0 39701 lflmul 39704 lkrlss 39731 dochexmid 42104 lcfl8 42138 lcd0vcl 42250 mapdh6bN 42373 mapdh6cN 42374 hdmap1val0 42435 hdmap1l6b 42447 hdmap1l6c 42448 hdmapval0 42469 hdmaprnlem17N 42499 hdmap14lem13 42516 hdmaplkr 42549 lcoel0 49059 |
| Copyright terms: Public domain | W3C validator |