Theorem lsppreli

Description: A vector expressed as a sum belongs to the span of its components. (Contributed by NM, 9-Apr-2015)

	Ref	Expression
Hypotheses	lsppreli.v	|- V = ( Base ` W )
	lsppreli.p	|- .+ = ( +g ` W )
	lsppreli.t	|- .x. = ( .s ` W )
	lsppreli.f	|- F = ( Scalar ` W )
	lsppreli.k	|- K = ( Base ` F )
	lsppreli.n	|- N = ( LSpan ` W )
	lsppreli.w	|- ( ph -> W e. LMod )
	lsppreli.a	|- ( ph -> A e. K )
	lsppreli.b	|- ( ph -> B e. K )
	lsppreli.x	|- ( ph -> X e. V )
	lsppreli.y	|- ( ph -> Y e. V )
Assertion	lsppreli	|- ( ph -> ( ( A .x. X ) .+ ( B .x. Y ) ) e. ( N ` { X , Y } ) )

Proof

Step	Hyp	Ref	Expression
1		lsppreli.v	|- V = ( Base ` W )
2		lsppreli.p	|- .+ = ( +g ` W )
3		lsppreli.t	|- .x. = ( .s ` W )
4		lsppreli.f	|- F = ( Scalar ` W )
5		lsppreli.k	|- K = ( Base ` F )
6		lsppreli.n	|- N = ( LSpan ` W )
7		lsppreli.w	|- ( ph -> W e. LMod )
8		lsppreli.a	|- ( ph -> A e. K )
9		lsppreli.b	|- ( ph -> B e. K )
10		lsppreli.x	|- ( ph -> X e. V )
11		lsppreli.y	|- ( ph -> Y e. V )
12	1 6	lspsnsubg	|- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) e. ( SubGrp ` W ) )
13	7 10 12	syl2anc	|- ( ph -> ( N ` { X } ) e. ( SubGrp ` W ) )
14	1 6	lspsnsubg	|- ( ( W e. LMod /\ Y e. V ) -> ( N ` { Y } ) e. ( SubGrp ` W ) )
15	7 11 14	syl2anc	|- ( ph -> ( N ` { Y } ) e. ( SubGrp ` W ) )
16	1 3 4 5 6 7 8 10	lspsneli	|- ( ph -> ( A .x. X ) e. ( N ` { X } ) )
17	1 3 4 5 6 7 9 11	lspsneli	|- ( ph -> ( B .x. Y ) e. ( N ` { Y } ) )
18		eqid	|- ( LSSum ` W ) = ( LSSum ` W )
19	2 18	lsmelvali	|- ( ( ( ( N ` { X } ) e. ( SubGrp ` W ) /\ ( N ` { Y } ) e. ( SubGrp ` W ) ) /\ ( ( A .x. X ) e. ( N ` { X } ) /\ ( B .x. Y ) e. ( N ` { Y } ) ) ) -> ( ( A .x. X ) .+ ( B .x. Y ) ) e. ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
20	13 15 16 17 19	syl22anc	|- ( ph -> ( ( A .x. X ) .+ ( B .x. Y ) ) e. ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
21	1 6 18 7 10 11	lsmpr	|- ( ph -> ( N ` { X , Y } ) = ( ( N ` { X } ) ( LSSum ` W ) ( N ` { Y } ) ) )
22	20 21	eleqtrrd	|- ( ph -> ( ( A .x. X ) .+ ( B .x. Y ) ) e. ( N ` { X , Y } ) )