Metamath Proof Explorer

Theorem ellcoellss

Description: Every linear combination of a subset of a linear subspace is also contained in the linear subspace. (Contributed by AV, 20-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Assertion ellcoellss ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ∀ 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) 𝑥 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → 𝑀 ∈ LMod )
2 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
3 eqid ⊢ ( LSubSp ‘ 𝑀 ) = ( LSubSp ‘ 𝑀 )
4 2 3 lssss ⊢ ( 𝑆 ∈ ( LSubSp ‘ 𝑀 ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
5 4 3ad2ant2 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → 𝑆 ⊆ ( Base ‘ 𝑀 ) )
6 sstr ⊢ ( ( 𝑉 ⊆ 𝑆 ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → 𝑉 ⊆ ( Base ‘ 𝑀 ) )
7 fvex ⊢ ( Base ‘ 𝑀 ) ∈ V
8 7 ssex ⊢ ( 𝑉 ⊆ ( Base ‘ 𝑀 ) → 𝑉 ∈ V )
9 elpwg ⊢ ( 𝑉 ∈ V → ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ↔ 𝑉 ⊆ ( Base ‘ 𝑀 ) ) )
10 9 biimprd ⊢ ( 𝑉 ∈ V → ( 𝑉 ⊆ ( Base ‘ 𝑀 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
11 8 10 mpcom ⊢ ( 𝑉 ⊆ ( Base ‘ 𝑀 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
12 6 11 syl ⊢ ( ( 𝑉 ⊆ 𝑆 ∧ 𝑆 ⊆ ( Base ‘ 𝑀 ) ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
13 12 ex ⊢ ( 𝑉 ⊆ 𝑆 → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
14 13 3ad2ant3 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ( 𝑆 ⊆ ( Base ‘ 𝑀 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) )
15 5 14 mpd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
16 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
17 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
18 2 16 17 lcoval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
19 1 15 18 syl2anc ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ( 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
20 lincellss ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ( ( 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ∈ 𝑆 ) )
21 20 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ ( 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ∈ 𝑆 )
22 eleq1 ⊢ ( 𝑥 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) → ( 𝑥 ∈ 𝑆 ↔ ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ∈ 𝑆 ) )
23 21 22 imbitrrid ⊢ ( 𝑥 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) → ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ ( 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → 𝑥 ∈ 𝑆 ) )
24 23 expd ⊢ ( 𝑥 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) → ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ( ( 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → 𝑥 ∈ 𝑆 ) ) )
25 24 com12 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ( 𝑥 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) → ( ( 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → 𝑥 ∈ 𝑆 ) ) )
26 25 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑥 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) → ( ( 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → 𝑥 ∈ 𝑆 ) ) )
27 26 com13 ⊢ ( ( 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑥 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) → ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → 𝑥 ∈ 𝑆 ) ) )
28 27 impr ⊢ ( ( 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → 𝑥 ∈ 𝑆 ) )
29 28 rexlimiva ⊢ ( ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ) → ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → 𝑥 ∈ 𝑆 ) )
30 29 com12 ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) ∧ 𝑥 ∈ ( Base ‘ 𝑀 ) ) → ( ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ) → 𝑥 ∈ 𝑆 ) )
31 30 expimpd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ( ( 𝑥 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑥 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → 𝑥 ∈ 𝑆 ) )
32 19 31 sylbid ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ( 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) → 𝑥 ∈ 𝑆 ) )
33 32 ralrimiv ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑆 ∈ ( LSubSp ‘ 𝑀 ) ∧ 𝑉 ⊆ 𝑆 ) → ∀ 𝑥 ∈ ( 𝑀 LinCo 𝑉 ) 𝑥 ∈ 𝑆 )