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

Metamath Proof Explorer

Theorem lspsnne2

Description: Two ways to express that vectors have different spans. (Contributed by NM, 20-May-2015)

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

Proof

Step Hyp Ref Expression
1 lspsnne2.v 
 |-  V = ( Base ` W )
2 lspsnne2.n 
 |-  N = ( LSpan ` W )
3 lspsnne2.w 
 |-  ( ph -> W e. LMod )
4 lspsnne2.x 
 |-  ( ph -> X e. V )
5 lspsnne2.y 
 |-  ( ph -> Y e. V )
6 lspsnne2.e 
 |-  ( ph -> -. X e. ( N ` { Y } ) )
7 eqimss 
 |-  ( ( N ` { X } ) = ( N ` { Y } ) -> ( N ` { X } ) C_ ( N ` { Y } ) )
8 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
9 1 8 2 lspsncl 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
10 3 5 9 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
11 1 8 2 3 10 4 ellspsn5b 
 |-  ( ph -> ( X e. ( N ` { Y } ) <-> ( N ` { X } ) C_ ( N ` { Y } ) ) )
12 7 11 imbitrrid 
 |-  ( ph -> ( ( N ` { X } ) = ( N ` { Y } ) -> X e. ( N ` { Y } ) ) )
13 12 necon3bd 
 |-  ( ph -> ( -. X e. ( N ` { Y } ) -> ( N ` { X } ) =/= ( N ` { Y } ) ) )
14 6 13 mpd 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )