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

Metamath Proof Explorer

Theorem lspprid1

Description: A member of a pair of vectors belongs to their span. (Contributed by NM, 14-May-2015)

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

Proof

Step Hyp Ref Expression
1 lspprid.v 
 |-  V = ( Base ` W )
2 lspprid.n 
 |-  N = ( LSpan ` W )
3 lspprid.w 
 |-  ( ph -> W e. LMod )
4 lspprid.x 
 |-  ( ph -> X e. V )
5 lspprid.y 
 |-  ( ph -> Y e. V )
6 4 5 prssd 
 |-  ( ph -> { X , Y } C_ V )
7 snsspr1 
 |-  { X } C_ { X , Y }
8 7 a1i 
 |-  ( ph -> { X } C_ { X , Y } )
9 1 2 lspss 
 |-  ( ( W e. LMod /\ { X , Y } C_ V /\ { X } C_ { X , Y } ) -> ( N ` { X } ) C_ ( N ` { X , Y } ) )
10 3 6 8 9 syl3anc 
 |-  ( ph -> ( N ` { X } ) C_ ( N ` { X , Y } ) )
11 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
12 1 11 2 3 4 5 lspprcl 
 |-  ( ph -> ( N ` { X , Y } ) e. ( LSubSp ` W ) )
13 1 11 2 3 12 4 ellspsn5b 
 |-  ( ph -> ( X e. ( N ` { X , Y } ) <-> ( N ` { X } ) C_ ( N ` { X , Y } ) ) )
14 10 13 mpbird 
 |-  ( ph -> X e. ( N ` { X , Y } ) )