lmod0vcl - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > lmod0vcl		GIF version

Theorem lmod0vcl 14637

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

Colors of variables: wff set class

Syntax hints: → wi 4 = wceq 1402 ∈ wcel 2209 ‘cfv 5375 Basecbs 13335 0_gc0g 13593 Grpcgrp 13788 LModclmod 14606

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-sep 4247 ax-pow 4309 ax-pr 4344 ax-un 4576 ax-cnex 8264 ax-resscn 8265 ax-1re 8267 ax-addrcl 8270

This theorem depends on definitions: df-bi 117 df-3an 1011 df-tru 1405 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-un 3224 df-in 3226 df-ss 3233 df-pw 3690 df-sn 3714 df-pr 3715 df-op 3717 df-uni 3934 df-int 3969 df-br 4129 df-opab 4191 df-mpt 4192 df-id 4436 df-xp 4778 df-rel 4779 df-cnv 4780 df-co 4781 df-dm 4782 df-rn 4783 df-res 4784 df-iota 5335 df-fun 5377 df-fn 5378 df-fv 5383 df-riota 6032 df-ov 6082 df-inn 9288 df-2 9346 df-3 9347 df-4 9348 df-5 9349 df-6 9350 df-ndx 13338 df-slot 13339 df-base 13341 df-plusg 13427 df-mulr 13428 df-sca 13430 df-vsca 13431 df-0g 13595 df-mgm 13659 df-sgrp 13700 df-mnd 13713 df-grp 13791 df-lmod 14608

This theorem is referenced by: lmodvs0 14642 lmodfopne 14646 lss1 14682 lsssn0 14690 lssintclm 14704 lspuni0 14744 lspun0 14745 lss0v 14750