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 M LMod S LSubSp M V S x M LinCo V x S

Proof

Step Hyp Ref Expression
1 simp1 M LMod S LSubSp M V S M LMod
2 eqid Base M = Base M
3 eqid LSubSp M = LSubSp M
4 2 3 lssss S LSubSp M S Base M
5 4 3ad2ant2 M LMod S LSubSp M V S S Base M
6 sstr V S S Base M V Base M
7 fvex Base M V
8 7 ssex V Base M V V
9 elpwg V V V 𝒫 Base M V Base M
10 9 biimprd V V V Base M V 𝒫 Base M
11 8 10 mpcom V Base M V 𝒫 Base M
12 6 11 syl V S S Base M V 𝒫 Base M
13 12 ex V S S Base M V 𝒫 Base M
14 13 3ad2ant3 M LMod S LSubSp M V S S Base M V 𝒫 Base M
15 5 14 mpd M LMod S LSubSp M V S V 𝒫 Base M
16 eqid Scalar M = Scalar M
17 eqid Base Scalar M = Base Scalar M
18 2 16 17 lcoval M LMod V 𝒫 Base M x M LinCo V x Base M f Base Scalar M V finSupp 0 Scalar M f x = f linC M V
19 1 15 18 syl2anc M LMod S LSubSp M V S x M LinCo V x Base M f Base Scalar M V finSupp 0 Scalar M f x = f linC M V
20 lincellss M LMod S LSubSp M V S f Base Scalar M V finSupp 0 Scalar M f f linC M V S
21 20 imp M LMod S LSubSp M V S f Base Scalar M V finSupp 0 Scalar M f f linC M V S
22 eleq1 x = f linC M V x S f linC M V S
23 21 22 syl5ibr x = f linC M V M LMod S LSubSp M V S f Base Scalar M V finSupp 0 Scalar M f x S
24 23 expd x = f linC M V M LMod S LSubSp M V S f Base Scalar M V finSupp 0 Scalar M f x S
25 24 com12 M LMod S LSubSp M V S x = f linC M V f Base Scalar M V finSupp 0 Scalar M f x S
26 25 adantr M LMod S LSubSp M V S x Base M x = f linC M V f Base Scalar M V finSupp 0 Scalar M f x S
27 26 com13 f Base Scalar M V finSupp 0 Scalar M f x = f linC M V M LMod S LSubSp M V S x Base M x S
28 27 impr f Base Scalar M V finSupp 0 Scalar M f x = f linC M V M LMod S LSubSp M V S x Base M x S
29 28 rexlimiva f Base Scalar M V finSupp 0 Scalar M f x = f linC M V M LMod S LSubSp M V S x Base M x S
30 29 com12 M LMod S LSubSp M V S x Base M f Base Scalar M V finSupp 0 Scalar M f x = f linC M V x S
31 30 expimpd M LMod S LSubSp M V S x Base M f Base Scalar M V finSupp 0 Scalar M f x = f linC M V x S
32 19 31 sylbid M LMod S LSubSp M V S x M LinCo V x S
33 32 ralrimiv M LMod S LSubSp M V S x M LinCo V x S