# Metamath Proof Explorer

## Theorem lmodindp1

Description: Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015)

Ref Expression
Hypotheses lmodindp1.v
`|- V = ( Base ` W )`
lmodindp1.p
`|- .+ = ( +g ` W )`
lmodindp1.o
`|- .0. = ( 0g ` W )`
lmodindp1.n
`|- N = ( LSpan ` W )`
lmodindp1.w
`|- ( ph -> W e. LMod )`
lmodindp1.x
`|- ( ph -> X e. V )`
lmodindp1.y
`|- ( ph -> Y e. V )`
lmodindp1.q
`|- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )`
Assertion lmodindp1
`|- ( ph -> ( X .+ Y ) =/= .0. )`

### Proof

Step Hyp Ref Expression
1 lmodindp1.v
` |-  V = ( Base ` W )`
2 lmodindp1.p
` |-  .+ = ( +g ` W )`
3 lmodindp1.o
` |-  .0. = ( 0g ` W )`
4 lmodindp1.n
` |-  N = ( LSpan ` W )`
5 lmodindp1.w
` |-  ( ph -> W e. LMod )`
6 lmodindp1.x
` |-  ( ph -> X e. V )`
7 lmodindp1.y
` |-  ( ph -> Y e. V )`
8 lmodindp1.q
` |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )`
9 eqid
` |-  ( invg ` W ) = ( invg ` W )`
10 1 9 4 lspsnneg
` |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { ( ( invg ` W ) ` X ) } ) = ( N ` { X } ) )`
11 5 6 10 syl2anc
` |-  ( ph -> ( N ` { ( ( invg ` W ) ` X ) } ) = ( N ` { X } ) )`
12 11 eqcomd
` |-  ( ph -> ( N ` { X } ) = ( N ` { ( ( invg ` W ) ` X ) } ) )`
` |-  ( ( ph /\ ( X .+ Y ) = .0. ) -> ( N ` { X } ) = ( N ` { ( ( invg ` W ) ` X ) } ) )`
14 lmodgrp
` |-  ( W e. LMod -> W e. Grp )`
15 5 14 syl
` |-  ( ph -> W e. Grp )`
16 1 2 3 9 grpinvid1
` |-  ( ( W e. Grp /\ X e. V /\ Y e. V ) -> ( ( ( invg ` W ) ` X ) = Y <-> ( X .+ Y ) = .0. ) )`
17 15 6 7 16 syl3anc
` |-  ( ph -> ( ( ( invg ` W ) ` X ) = Y <-> ( X .+ Y ) = .0. ) )`
18 17 biimpar
` |-  ( ( ph /\ ( X .+ Y ) = .0. ) -> ( ( invg ` W ) ` X ) = Y )`
19 18 sneqd
` |-  ( ( ph /\ ( X .+ Y ) = .0. ) -> { ( ( invg ` W ) ` X ) } = { Y } )`
20 19 fveq2d
` |-  ( ( ph /\ ( X .+ Y ) = .0. ) -> ( N ` { ( ( invg ` W ) ` X ) } ) = ( N ` { Y } ) )`
21 13 20 eqtrd
` |-  ( ( ph /\ ( X .+ Y ) = .0. ) -> ( N ` { X } ) = ( N ` { Y } ) )`
22 21 ex
` |-  ( ph -> ( ( X .+ Y ) = .0. -> ( N ` { X } ) = ( N ` { Y } ) ) )`
23 22 necon3d
` |-  ( ph -> ( ( N ` { X } ) =/= ( N ` { Y } ) -> ( X .+ Y ) =/= .0. ) )`
24 8 23 mpd
` |-  ( ph -> ( X .+ Y ) =/= .0. )`