Metamath Proof Explorer

Theorem lincellss

Description: A linear combination of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019) (Revised by AV, 28-Jul-2019)

Ref Expression
Assertion lincellss ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ( ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) ∈ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → 𝑀 ∈ LMod )
2 simprl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
3 ssexg ⊢ ( ( 𝑉 ⊆ 𝑆 ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ) → 𝑉 ∈ V )
4 3 ancoms ⊢ ( ( 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → 𝑉 ∈ V )
5 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
6 eqid ⊢ ( LSubSp ‘ 𝑀 ) = ( LSubSp ‘ 𝑀 )
7 5 6 lssss ⊢ ( 𝑆 ∈ ( LSubSp ‘ 𝑀 ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
8 sstr ⊢ ( ( 𝑉 ⊆ 𝑆 ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → 𝑉 ⊆ ( Base ‘ 𝑀 ) )
9 elpwg ⊢ ( 𝑉 ∈ V → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ 𝑉 ⊆ ( Base ‘ 𝑀 ) ) )
10 8 9 syl5ibrcom ⊢ ( ( 𝑉 ⊆ 𝑆 ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → ( 𝑉 ∈ V → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
11 10 expcom ⊢ ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → ( 𝑉 ⊆ 𝑆 → ( 𝑉 ∈ V → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) )
12 7 11 syl ⊢ ( 𝑆 ∈ ( LSubSp ‘ 𝑀 ) → ( 𝑉 ⊆ 𝑆 → ( 𝑉 ∈ V → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) )
13 12 imp ⊢ ( ( 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ( 𝑉 ∈ V → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
14 4 13 mpd ⊢ ( ( 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
15 14 3adant1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
16 15 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
17 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
18 1 2 16 17 syl3anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
19 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
20 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
21 6 19 20 gsumlsscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ( ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ∈ 𝑆 ) )
22 21 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) ∈ 𝑆 )
23 18 22 eqeltrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) ∈ 𝑆 )
24 23 ex ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ( ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝐹 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) ∈ 𝑆 ) )