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

Metamath Proof Explorer

Theorem lsmelpr

Description: Two ways to say that a vector belongs to the span of a pair of vectors. (Contributed by NM, 14-Jan-2015)

Ref Expression
Hypotheses lsmelpr.v 
|- V = ( Base ` W )
lsmelpr.n 
|- N = ( LSpan ` W )
lsmelpr.p 
|- .(+) = ( LSSum ` W )
lsmelpr.w 
|- ( ph -> W e. LMod )
lsmelpr.x 
|- ( ph -> X e. V )
lsmelpr.y 
|- ( ph -> Y e. V )
lsmelpr.z 
|- ( ph -> Z e. V )
Assertion lsmelpr 
|- ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) ) )

Proof

Step Hyp Ref Expression
1 lsmelpr.v 
 |-  V = ( Base ` W )
2 lsmelpr.n 
 |-  N = ( LSpan ` W )
3 lsmelpr.p 
 |-  .(+) = ( LSSum ` W )
4 lsmelpr.w 
 |-  ( ph -> W e. LMod )
5 lsmelpr.x 
 |-  ( ph -> X e. V )
6 lsmelpr.y 
 |-  ( ph -> Y e. V )
7 lsmelpr.z 
 |-  ( ph -> Z e. V )
8 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
9 1 8 2 4 6 7 lspprcl 
 |-  ( ph -> ( N ` { Y , Z } ) e. ( LSubSp ` W ) )
10 1 8 2 4 9 5 ellspsn5b 
 |-  ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( N ` { Y , Z } ) ) )
11 1 2 3 4 6 7 lsmpr 
 |-  ( ph -> ( N ` { Y , Z } ) = ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) )
12 11 sseq2d 
 |-  ( ph -> ( ( N ` { X } ) C_ ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) ) )
13 10 12 bitrd 
 |-  ( ph -> ( X e. ( N ` { Y , Z } ) <-> ( N ` { X } ) C_ ( ( N ` { Y } ) .(+) ( N ` { Z } ) ) ) )