Theorem lspsneq0b

Description: Equal singleton spans imply both arguments are zero or both are nonzero. (Contributed by NM, 21-Mar-2015)

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

Proof

Step	Hyp	Ref	Expression
1		lspsneq0b.v	|- V = ( Base ` W )
2		lspsneq0b.o	|- .0. = ( 0g ` W )
3		lspsneq0b.n	|- N = ( LSpan ` W )
4		lspsneq0b.w	|- ( ph -> W e. LMod )
5		lspsneq0b.x	|- ( ph -> X e. V )
6		lspsneq0b.y	|- ( ph -> Y e. V )
7		lspsneq0b.e	|- ( ph -> ( N ` { X } ) = ( N ` { Y } ) )
8	7	adantr	|- ( ( ph /\ X = .0. ) -> ( N ` { X } ) = ( N ` { Y } ) )
9	1 2 3	lspsneq0	|- ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )
10	4 5 9	syl2anc	|- ( ph -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )
11	10	biimpar	|- ( ( ph /\ X = .0. ) -> ( N ` { X } ) = { .0. } )
12	8 11	eqtr3d	|- ( ( ph /\ X = .0. ) -> ( N ` { Y } ) = { .0. } )
13	1 2 3	lspsneq0	|- ( ( W e. LMod /\ Y e. V ) -> ( ( N ` { Y } ) = { .0. } <-> Y = .0. ) )
14	4 6 13	syl2anc	|- ( ph -> ( ( N ` { Y } ) = { .0. } <-> Y = .0. ) )
15	14	adantr	|- ( ( ph /\ X = .0. ) -> ( ( N ` { Y } ) = { .0. } <-> Y = .0. ) )
16	12 15	mpbid	|- ( ( ph /\ X = .0. ) -> Y = .0. )
17	7	adantr	|- ( ( ph /\ Y = .0. ) -> ( N ` { X } ) = ( N ` { Y } ) )
18	14	biimpar	|- ( ( ph /\ Y = .0. ) -> ( N ` { Y } ) = { .0. } )
19	17 18	eqtrd	|- ( ( ph /\ Y = .0. ) -> ( N ` { X } ) = { .0. } )
20	10	adantr	|- ( ( ph /\ Y = .0. ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )
21	19 20	mpbid	|- ( ( ph /\ Y = .0. ) -> X = .0. )
22	16 21	impbida	|- ( ph -> ( X = .0. <-> Y = .0. ) )