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 biimtrdi ⊢ ( ( 𝑀 ∈ 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 ‘ 𝑀 ) )