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