Metamath Proof Explorer


Theorem lincolss

Description: According to the statement in Lang p. 129, the set ( LSubSpM ) of all linear combinations of a set of vectors V is a submodule (_generated_ by V) of the module M. The elements of V are called generators of ( LSubSpM ) . (Contributed by AV, 12-Apr-2019)

Ref Expression
Assertion lincolss ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 LinCo 𝑉 ) ∈ ( LSubSp ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 eqidd ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 ) )
2 eqidd ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
3 eqidd ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 ) )
4 eqidd ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( +g𝑀 ) = ( +g𝑀 ) )
5 eqidd ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ·𝑠𝑀 ) = ( ·𝑠𝑀 ) )
6 eqidd ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( LSubSp ‘ 𝑀 ) = ( LSubSp ‘ 𝑀 ) )
7 eqid ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
8 eqid ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
9 eqid ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
10 7 8 9 lcoval ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑣 ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
11 simpl ( ( 𝑣 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) → 𝑣 ∈ ( Base ‘ 𝑀 ) )
12 10 11 syl6bi ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑣 ∈ ( 𝑀 LinCo 𝑉 ) → 𝑣 ∈ ( Base ‘ 𝑀 ) ) )
13 12 ssrdv ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 LinCo 𝑉 ) ⊆ ( Base ‘ 𝑀 ) )
14 lcoel0 ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 0g𝑀 ) ∈ ( 𝑀 LinCo 𝑉 ) )
15 14 ne0d ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 LinCo 𝑉 ) ≠ ∅ )
16 eqid ( ·𝑠𝑀 ) = ( ·𝑠𝑀 )
17 eqid ( +g𝑀 ) = ( +g𝑀 )
18 16 9 17 lincsumscmcl ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ ( 𝑥 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑎 ∈ ( 𝑀 LinCo 𝑉 ) ∧ 𝑏 ∈ ( 𝑀 LinCo 𝑉 ) ) ) → ( ( 𝑥 ( ·𝑠𝑀 ) 𝑎 ) ( +g𝑀 ) 𝑏 ) ∈ ( 𝑀 LinCo 𝑉 ) )
19 1 2 3 4 5 6 13 15 18 islssd ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 LinCo 𝑉 ) ∈ ( LSubSp ‘ 𝑀 ) )