Metamath Proof Explorer

Theorem lincvalsc0

Description: The linear combination where all scalars are 0. (Contributed by AV, 12-Apr-2019)

Ref Expression
Hypotheses lincvalsc0.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
lincvalsc0.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
lincvalsc0.0 ⊢ 0 = ( 0g ‘ 𝑆 )
lincvalsc0.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
lincvalsc0.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ 0 )
Assertion lincvalsc0 ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 lincvalsc0.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 lincvalsc0.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
3 lincvalsc0.0 ⊢ 0 = ( 0g ‘ 𝑆 )
4 lincvalsc0.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
5 lincvalsc0.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ 0 )
6 simpl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑀 ∈ LMod )
7 2 eqcomi ⊢ ( Scalar ‘ 𝑀 ) = 𝑆
8 7 fveq2i ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ 𝑆 )
9 2 8 3 lmod0cl ⊢ ( 𝑀 ∈ LMod → 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
10 9 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
11 10 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) → 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
12 11 5 fmptd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
13 fvexd ⊢ ( 𝑀 ∈ LMod → ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V )
14 elmapg ⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
15 13 14 sylan ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
16 12 15 mpbird ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
17 1 pweqi ⊢ 𝒫 𝐵 = 𝒫 ( Base ‘ 𝑀 )
18 17 eleq2i ⊢ ( 𝑉 ∈ 𝒫 𝐵 ↔ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
19 18 bilani ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
20 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
21 6 16 19 20 syl3anc ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
22 simpr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
23 3 fvexi ⊢ 0 ∈ V
24 eqidd ⊢ ( 𝑥 = 𝑣 → 0 = 0 )
25 24 5 fvmptg ⊢ ( ( 𝑣 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝐹 ‘ 𝑣 ) = 0 )
26 22 23 25 sylancl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) = 0 )
27 26 oveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
28 6 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑀 ∈ LMod )
29 elelpwi ⊢ ( ( 𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑣 ∈ 𝐵 )
30 29 expcom ⊢ ( 𝑉 ∈ 𝒫 𝐵 → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
31 30 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
32 31 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝐵 )
33 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
34 1 2 33 3 4 lmod0vs ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ 𝐵 ) → ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
35 28 32 34 syl2anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
36 27 35 eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
37 36 mpteq2dva ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) )
38 37 oveq2d ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) ) )
39 lmodgrp ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
40 39 grpmndd ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Mnd )
41 4 gsumz ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) ) = 𝑍 )
42 40 41 sylan ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) ) = 𝑍 )
43 21 38 42 3eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = 𝑍 )