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

Metamath Proof Explorer

Theorem ellspsni

Description: A scalar product with a vector belongs to the span of its singleton. ( spansnmul analog.) (Contributed by NM, 2-Jul-2014)

Ref Expression
Hypotheses lspsnvsel.v 
|- V = ( Base ` W )
lspsnvsel.t 
|- .x. = ( .s ` W )
lspsnvsel.f 
|- F = ( Scalar ` W )
lspsnvsel.k 
|- K = ( Base ` F )
lspsnvsel.n 
|- N = ( LSpan ` W )
lspsnvsel.w 
|- ( ph -> W e. LMod )
lspsnvsel.a 
|- ( ph -> A e. K )
lspsnvsel.x 
|- ( ph -> X e. V )
Assertion ellspsni 
|- ( ph -> ( A .x. X ) e. ( N ` { X } ) )

Proof

Step Hyp Ref Expression
1 lspsnvsel.v 
 |-  V = ( Base ` W )
2 lspsnvsel.t 
 |-  .x. = ( .s ` W )
3 lspsnvsel.f 
 |-  F = ( Scalar ` W )
4 lspsnvsel.k 
 |-  K = ( Base ` F )
5 lspsnvsel.n 
 |-  N = ( LSpan ` W )
6 lspsnvsel.w 
 |-  ( ph -> W e. LMod )
7 lspsnvsel.a 
 |-  ( ph -> A e. K )
8 lspsnvsel.x 
 |-  ( ph -> X e. V )
9 eqid 
 |-  ( LSubSp ` W ) = ( LSubSp ` W )
10 1 9 5 lspsncl 
 |-  ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( LSubSp ` W ) )
11 6 8 10 syl2anc 
 |-  ( ph -> ( N ` { X } ) e. ( LSubSp ` W ) )
12 1 5 lspsnid 
 |-  ( ( W e. LMod /\ X e. V ) -> X e. ( N ` { X } ) )
13 6 8 12 syl2anc 
 |-  ( ph -> X e. ( N ` { X } ) )
14 3 2 4 9 lssvscl 
 |-  ( ( ( W e. LMod /\ ( N ` { X } ) e. ( LSubSp ` W ) ) /\ ( A e. K /\ X e. ( N ` { X } ) ) ) -> ( A .x. X ) e. ( N ` { X } ) )
15 6 11 7 13 14 syl22anc 
 |-  ( ph -> ( A .x. X ) e. ( N ` { X } ) )