Metamath Proof Explorer

Theorem lcoss

Description: A set of vectors of a module is a subset of the set of all linear combinations of the set. (Contributed by AV, 18-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Assertion lcoss ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑉 ⊆ ( 𝑀 LinCo 𝑉 ) )

Proof

Step Hyp Ref Expression
1 elelpwi ⊢ ( ( 𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑣 ∈ ( Base ‘ 𝑀 ) )
2 1 expcom ⊢ ( 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ ( Base ‘ 𝑀 ) ) )
3 2 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ ( Base ‘ 𝑀 ) ) )
4 3 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ ( Base ‘ 𝑀 ) )
5 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
6 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
7 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) )
8 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑀 ) ) = ( 1r ‘ ( Scalar ‘ 𝑀 ) )
9 equequ1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑣 ↔ 𝑦 = 𝑣 ) )
10 9 ifbid ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) = if ( 𝑦 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
11 10 cbvmptv ⊢ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) = ( 𝑦 ∈ 𝑉 ↦ if ( 𝑦 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
12 5 6 7 8 11 mptcfsupp ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
13 12 3expa ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
14 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
15 5 6 7 8 14 linc1 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) = 𝑣 )
16 15 3expa ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) = 𝑣 )
17 16 eqcomd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 = ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) )
18 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
19 6 18 8 lmod1cl ⊢ ( 𝑀 ∈ LMod → ( 1r ‘ ( Scalar ‘ 𝑀 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
20 6 18 7 lmod0cl ⊢ ( 𝑀 ∈ LMod → ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
21 19 20 ifcld ⊢ ( 𝑀 ∈ LMod → if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
22 21 ad3antrrr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑥 ∈ 𝑉 ) → if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
23 22 fmpttd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
24 fvex ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V
25 simplr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
26 elmapg ⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
27 24 25 26 sylancr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
28 23 27 mpbird ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
29 breq1 ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
30 oveq1 ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) = ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) )
31 30 eqeq2d ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( 𝑣 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ↔ 𝑣 = ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) ) )
32 29 31 anbi12d ⊢ ( 𝑓 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ) ↔ ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
33 32 adantl ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑓 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ) → ( ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ) ↔ ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
34 28 33 rspcedv ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑣 , ( 1r ‘ ( Scalar ‘ 𝑀 ) ) , ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) ) → ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
35 13 17 34 mp2and ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ) )
36 5 6 18 lcoval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑣 ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
37 36 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝑣 ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( 𝑣 ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑓 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑓 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ 𝑣 = ( 𝑓 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
38 4 35 37 mpbir2and ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ ( 𝑀 LinCo 𝑉 ) )
39 38 ex ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ ( 𝑀 LinCo 𝑉 ) ) )
40 39 ssrdv ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → 𝑉 ⊆ ( 𝑀 LinCo 𝑉 ) )