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. )