This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) } ) )
13 12 adantr 
 |-  ( ( 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. )