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 lspsnel5
 |-  ( 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 } ) ) ) )