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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lsppreli.p	⊢ + = ( +_g ‘ 𝑊 )
	lsppreli.t	⊢ · = ( ·_𝑠 ‘ 𝑊 )
	lsppreli.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	lsppreli.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	lsppreli.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lsppreli.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
	lsppreli.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
	lsppreli.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
	lsppreli.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lsppreli.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
Assertion	lsppreli	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )

Proof

Step	Hyp	Ref	Expression
1		lsppreli.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lsppreli.p	⊢ + = ( +_g ‘ 𝑊 )
3		lsppreli.t	⊢ · = ( ·_𝑠 ‘ 𝑊 )
4		lsppreli.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5		lsppreli.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
6		lsppreli.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
7		lsppreli.w	⊢ ( 𝜑 → 𝑊 ∈ LMod )
8		lsppreli.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐾 )
9		lsppreli.b	⊢ ( 𝜑 → 𝐵 ∈ 𝐾 )
10		lsppreli.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
11		lsppreli.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
12	1 6	lspsnsubg	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
13	7 10 12	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) )
14	1 6	lspsnsubg	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
15	7 11 14	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) )
16	1 3 4 5 6 7 8 10	ellspsni	⊢ ( 𝜑 → ( 𝐴 · 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) )
17	1 3 4 5 6 7 9 11	ellspsni	⊢ ( 𝜑 → ( 𝐵 · 𝑌 ) ∈ ( 𝑁 ‘ { 𝑌 } ) )
18		eqid	⊢ ( LSSum ‘ 𝑊 ) = ( LSSum ‘ 𝑊 )
19	2 18	lsmelvali	⊢ ( ( ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑊 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( SubGrp ‘ 𝑊 ) ) ∧ ( ( 𝐴 · 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 } ) ∧ ( 𝐵 · 𝑌 ) ∈ ( 𝑁 ‘ { 𝑌 } ) ) ) → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) ∈ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
20	13 15 16 17 19	syl22anc	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) ∈ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
21	1 6 18 7 10 11	lsmpr	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑊 ) ( 𝑁 ‘ { 𝑌 } ) ) )
22	20 21	eleqtrrd	⊢ ( 𝜑 → ( ( 𝐴 · 𝑋 ) + ( 𝐵 · 𝑌 ) ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )

Metamath Proof Explorer

Theorem lsppreli

Proof