Metamath Proof Explorer

Theorem lcoel0

Description: The zero vector is always a linear combination. (Contributed by AV, 12-Apr-2019) (Proof shortened by AV, 30-Jul-2019)

Ref Expression
Assertion lcoel0 ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 0g ‘ 𝑀 ) ∈ ( 𝑀 LinCo 𝑉 ) )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( 0g ‘ 𝑀 ) ∈ V
2 1 snid ⊢ ( 0g ‘ 𝑀 ) ∈ { ( 0g ‘ 𝑀 ) }
3 oveq2 ⊢ ( 𝑉 = ∅ → ( 𝑀 LinCo 𝑉 ) = ( 𝑀 LinCo ∅ ) )
4 lmodgrp ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
5 grpmnd ⊢ ( 𝑀 ∈ Grp → 𝑀 ∈ Mnd )
6 lco0 ⊢ ( 𝑀 ∈ Mnd → ( 𝑀 LinCo ∅ ) = { ( 0g ‘ 𝑀 ) } )
7 4 5 6 3syl ⊢ ( 𝑀 ∈ LMod → ( 𝑀 LinCo ∅ ) = { ( 0g ‘ 𝑀 ) } )
8 7 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝑀 LinCo ∅ ) = { ( 0g ‘ 𝑀 ) } )
9 3 8 sylan9eq ⊢ ( ( 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 𝑀 LinCo 𝑉 ) = { ( 0g ‘ 𝑀 ) } )
10 2 9 eleqtrrid ⊢ ( ( 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 0g ‘ 𝑀 ) ∈ ( 𝑀 LinCo 𝑉 ) )
11 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
12 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
13 11 12 lmod0vcl ⊢ ( 𝑀 ∈ LMod → ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) )
14 13 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) )
15 14 adantl ⊢ ( ( ¬ 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) )
16 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
17 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) )
18 eqidd ⊢ ( 𝑣 = 𝑤 → ( 0g ‘ ( Scalar ‘ 𝑀 ) ) = ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
19 18 cbvmptv ⊢ ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) = ( 𝑤 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) )
20 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ ( Scalar ‘ 𝑀 ) )
21 11 16 17 12 19 20 lcoc0 ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 0g ‘ 𝑀 ) ) )
22 21 adantl ⊢ ( ( ¬ 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 0g ‘ 𝑀 ) ) )
23 simpl ⊢ ( ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( ¬ 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) ) → ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
24 breq1 ⊢ ( 𝑠 = ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ↔ ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) )
25 oveq1 ⊢ ( 𝑠 = ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) = ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) )
26 25 eqeq2d ⊢ ( 𝑠 = ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( ( 0g ‘ 𝑀 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ↔ ( 0g ‘ 𝑀 ) = ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) ) )
27 eqcom ⊢ ( ( 0g ‘ 𝑀 ) = ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) ↔ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 0g ‘ 𝑀 ) )
28 26 27 bitrdi ⊢ ( 𝑠 = ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( ( 0g ‘ 𝑀 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ↔ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 0g ‘ 𝑀 ) ) )
29 24 28 anbi12d ⊢ ( 𝑠 = ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) → ( ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 0g ‘ 𝑀 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ↔ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 0g ‘ 𝑀 ) ) ) )
30 29 adantl ⊢ ( ( ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( ¬ 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) ) ∧ 𝑠 = ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ) → ( ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 0g ‘ 𝑀 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ↔ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 0g ‘ 𝑀 ) ) ) )
31 23 30 rspcedv ⊢ ( ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( ¬ 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) ) → ( ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 0g ‘ 𝑀 ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 0g ‘ 𝑀 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
32 31 ex ⊢ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) → ( ( ¬ 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 0g ‘ 𝑀 ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 0g ‘ 𝑀 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
33 32 com23 ⊢ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) → ( ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 0g ‘ 𝑀 ) ) → ( ( ¬ 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 0g ‘ 𝑀 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
34 33 3impib ⊢ ( ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( ( 𝑣 ∈ 𝑉 ↦ ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ) ( linC ‘ 𝑀 ) 𝑉 ) = ( 0g ‘ 𝑀 ) ) → ( ( ¬ 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 0g ‘ 𝑀 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) )
35 22 34 mpcom ⊢ ( ( ¬ 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 0g ‘ 𝑀 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) )
36 11 16 20 lcoval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( ( 0g ‘ 𝑀 ) ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 0g ‘ 𝑀 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
37 36 adantl ⊢ ( ( ¬ 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( ( 0g ‘ 𝑀 ) ∈ ( 𝑀 LinCo 𝑉 ) ↔ ( ( 0g ‘ 𝑀 ) ∈ ( Base ‘ 𝑀 ) ∧ ∃ 𝑠 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ( 𝑠 finSupp ( 0g ‘ ( Scalar ‘ 𝑀 ) ) ∧ ( 0g ‘ 𝑀 ) = ( 𝑠 ( linC ‘ 𝑀 ) 𝑉 ) ) ) ) )
38 15 35 37 mpbir2and ⊢ ( ( ¬ 𝑉 = ∅ ∧ ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) ) → ( 0g ‘ 𝑀 ) ∈ ( 𝑀 LinCo 𝑉 ) )
39 10 38 pm2.61ian ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 0g ‘ 𝑀 ) ∈ ( 𝑀 LinCo 𝑉 ) )