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

Metamath Proof Explorer

Theorem lspsnss2

Description: Comparable spans of singletons must have proportional vectors. See lspsneq for equal span version. (Contributed by NM, 7-Jun-2015)

Ref Expression
Hypotheses lspsnss2.v 
|- V = ( Base ` W )
lspsnss2.s 
|- S = ( Scalar ` W )
lspsnss2.k 
|- K = ( Base ` S )
lspsnss2.t 
|- .x. = ( .s ` W )
lspsnss2.n 
|- N = ( LSpan ` W )
lspsnss2.w 
|- ( ph -> W e. LMod )
lspsnss2.x 
|- ( ph -> X e. V )
lspsnss2.y 
|- ( ph -> Y e. V )
Assertion lspsnss2 
|- ( ph -> ( ( N ` { X } ) C_ ( N ` { Y } ) <-> E. k e. K X = ( k .x. Y ) ) )

Proof

Step Hyp Ref Expression
1 lspsnss2.v 
 |-  V = ( Base ` W )
2 lspsnss2.s 
 |-  S = ( Scalar ` W )
3 lspsnss2.k 
 |-  K = ( Base ` S )
4 lspsnss2.t 
 |-  .x. = ( .s ` W )
5 lspsnss2.n 
 |-  N = ( LSpan ` W )
6 lspsnss2.w 
 |-  ( ph -> W e. LMod )
7 lspsnss2.x 
 |-  ( ph -> X e. V )
8 lspsnss2.y 
 |-  ( ph -> Y e. V )
9 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
10 1 9 5 lspsncl 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( LSubSp ` W ) )
11 6 8 10 syl2anc 
 |-  ( ph -> ( N ` { Y } ) e. ( LSubSp ` W ) )
12 1 9 5 6 11 7 ellspsn5b 
 |-  ( ph -> ( X e. ( N ` { Y } ) <-> ( N ` { X } ) C_ ( N ` { Y } ) ) )
13 2 3 1 4 5 ellspsn 
 |-  ( ( W e. LMod /\ Y e. V ) -> ( X e. ( N ` { Y } ) <-> E. k e. K X = ( k .x. Y ) ) )
14 6 8 13 syl2anc 
 |-  ( ph -> ( X e. ( N ` { Y } ) <-> E. k e. K X = ( k .x. Y ) ) )
15 12 14 bitr3d 
 |-  ( ph -> ( ( N ` { X } ) C_ ( N ` { Y } ) <-> E. k e. K X = ( k .x. Y ) ) )