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

Metamath Proof Explorer

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