lmodvnegid - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > lmodvnegid		Structured version Visualization version GIF version

Theorem lmodvnegid 20832

Description: Addition of a vector with its negative. (Contributed by NM, 18-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)

**Hypotheses**
Ref	Expression
lmodvnegid.v	⊢ 𝑉 = (Base‘𝑊)
lmodvnegid.p	⊢ + = (+_g‘𝑊)
lmodvnegid.z	⊢ 0 = (0_g‘𝑊)
lmodvnegid.n	⊢ 𝑁 = (inv_g‘𝑊)

**Assertion**
Ref	Expression
lmodvnegid	⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑋 + (𝑁‘𝑋)) = 0 )

**Proof of Theorem lmodvnegid**
Step	Hyp	Ref	Expression
1		lmodgrp 20795	. 2 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
2		lmodvnegid.v	. . 3 ⊢ 𝑉 = (Base‘𝑊)
3		lmodvnegid.p	. . 3 ⊢ + = (+_g‘𝑊)
4		lmodvnegid.z	. . 3 ⊢ 0 = (0_g‘𝑊)
5		lmodvnegid.n	. . 3 ⊢ 𝑁 = (inv_g‘𝑊)
6	2, 3, 4, 5	grprinv 18898	. 2 ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉) → (𝑋 + (𝑁‘𝑋)) = 0 )
7	1, 6	sylan 580	1 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → (𝑋 + (𝑁‘𝑋)) = 0 )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ‘cfv 6476 (class class class)co 7341 Basecbs 17115 +_gcplusg 17156 0_gc0g 17338 Grpcgrp 18841 inv_gcminusg 18842 LModclmod 20788

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-op 4578 df-uni 4855 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5506 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-fv 6484 df-riota 7298 df-ov 7344 df-0g 17340 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-grp 18844 df-minusg 18845 df-lmod 20790

This theorem is referenced by: lmodvneg1 20833 hdmapneg 41885 lincext3 48488

W3C validator