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

Metamath Proof Explorer

Theorem lspsnnecom

Description: Swap two vectors with different spans. (Contributed by NM, 20-May-2015)

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

Proof

Step Hyp Ref Expression
1 lspsnnecom.v 
 |-  V = ( Base ` W )
2 lspsnnecom.o 
 |-  .0. = ( 0g ` W )
3 lspsnnecom.n 
 |-  N = ( LSpan ` W )
4 lspsnnecom.w 
 |-  ( ph -> W e. LVec )
5 lspsnnecom.x 
 |-  ( ph -> X e. V )
6 lspsnnecom.y 
 |-  ( ph -> Y e. ( V \ { .0. } ) )
7 lspsnnecom.e 
 |-  ( ph -> -. X e. ( N ` { Y } ) )
8 lveclmod 
 |-  ( W e. LVec -> W e. LMod )
9 4 8 syl 
 |-  ( ph -> W e. LMod )
10 6 eldifad 
 |-  ( ph -> Y e. V )
11 1 3 9 5 10 7 lspsnne2 
 |-  ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )
12 11 necomd 
 |-  ( ph -> ( N ` { Y } ) =/= ( N ` { X } ) )
13 1 2 3 4 6 5 12 lspsnne1 
 |-  ( ph -> -. Y e. ( N ` { X } ) )