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 biimpi ⊢ ( 𝑉 ∈ 𝒫 𝐵 → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
20 19 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
21 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
22 6 16 20 21 syl3anc ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
23 simpr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
24 3 fvexi ⊢ 0 ∈ V
25 eqidd ⊢ ( 𝑥 = 𝑣 → 0 = 0 )
26 25 5 fvmptg ⊢ ( ( 𝑣 ∈ 𝑉 ∧ 0 ∈ V ) → ( 𝐹 ‘ 𝑣 ) = 0 )
27 23 24 26 sylancl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) = 0 )
28 27 oveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
29 6 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑀 ∈ LMod )
30 elelpwi ⊢ ( ( 𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑣 ∈ 𝐵 )
31 30 expcom ⊢ ( 𝑉 ∈ 𝒫 𝐵 → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
32 31 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
33 32 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝐵 )
34 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
35 1 2 34 3 4 lmod0vs ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ 𝐵 ) → ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
36 29 33 35 syl2anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
37 28 36 eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
38 37 mpteq2dva ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) )
39 38 oveq2d ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) ) )
40 lmodgrp ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
41 40 grpmndd ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Mnd )
42 4 gsumz ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) ) = 𝑍 )
43 41 42 sylan ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) ) = 𝑍 )
44 22 39 43 3eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = 𝑍 )