Metamath Proof Explorer

Theorem linc0scn0

Description: If a set contains the zero element of a module, there is a linear combination being 0 where not all scalars are 0. (Contributed by AV, 13-Apr-2019)

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

Proof

Step Hyp Ref Expression
1 linc0scn0.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 linc0scn0.s ⊢ 𝑆 = ( Scalar ‘ 𝑀 )
3 linc0scn0.0 ⊢ 0 = ( 0g ‘ 𝑆 )
4 linc0scn0.1 ⊢ 1 = ( 1r ‘ 𝑆 )
5 linc0scn0.z ⊢ 𝑍 = ( 0g ‘ 𝑀 )
6 linc0scn0.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ if ( 𝑥 = 𝑍 , 1 , 0 ) )
7 simpl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑀 ∈ LMod )
8 2 lmodring ⊢ ( 𝑀 ∈ LMod → 𝑆 ∈ Ring )
9 2 eqcomi ⊢ ( Scalar ‘ 𝑀 ) = 𝑆
10 9 fveq2i ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) = ( Base ‘ 𝑆 )
11 10 4 ringidcl ⊢ ( 𝑆 ∈ Ring → 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
12 10 3 ring0cl ⊢ ( 𝑆 ∈ Ring → 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
13 11 12 jca ⊢ ( 𝑆 ∈ Ring → ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
14 8 13 syl ⊢ ( 𝑀 ∈ LMod → ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
15 14 ad2antrr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) → ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
16 ifcl ⊢ ( ( 1 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∧ 0 ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) → if ( 𝑥 = 𝑍 , 1 , 0 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
17 15 16 syl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝑉 ) → if ( 𝑥 = 𝑍 , 1 , 0 ) ∈ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
18 17 6 fmptd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) )
19 fvex ⊢ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V
20 19 a1i ⊢ ( 𝑀 ∈ LMod → ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V )
21 elmapg ⊢ ( ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ∈ V ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
22 20 21 sylan ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ↔ 𝐹 : 𝑉 ⟶ ( Base ‘ ( Scalar ‘ 𝑀 ) ) ) )
23 18 22 mpbird ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) )
24 1 pweqi ⊢ 𝒫 𝐵 = 𝒫 ( Base ‘ 𝑀 )
25 24 eleq2i ⊢ ( 𝑉 ∈ 𝒫 𝐵 ↔ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
26 25 biimpi ⊢ ( 𝑉 ∈ 𝒫 𝐵 → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
27 26 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) )
28 lincval ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐹 ∈ ( ( Base ‘ ( Scalar ‘ 𝑀 ) ) ↑m 𝑉 ) ∧ 𝑉 ∈ 𝒫 ( Base ‘ 𝑀 ) ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
29 7 23 27 28 syl3anc ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) )
30 simpr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
31 4 fvexi ⊢ 1 ∈ V
32 3 fvexi ⊢ 0 ∈ V
33 31 32 ifex ⊢ if ( 𝑣 = 𝑍 , 1 , 0 ) ∈ V
34 eqeq1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 = 𝑍 ↔ 𝑣 = 𝑍 ) )
35 34 ifbid ⊢ ( 𝑥 = 𝑣 → if ( 𝑥 = 𝑍 , 1 , 0 ) = if ( 𝑣 = 𝑍 , 1 , 0 ) )
36 35 6 fvmptg ⊢ ( ( 𝑣 ∈ 𝑉 ∧ if ( 𝑣 = 𝑍 , 1 , 0 ) ∈ V ) → ( 𝐹 ‘ 𝑣 ) = if ( 𝑣 = 𝑍 , 1 , 0 ) )
37 30 33 36 sylancl ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑣 ) = if ( 𝑣 = 𝑍 , 1 , 0 ) )
38 37 oveq1d ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( if ( 𝑣 = 𝑍 , 1 , 0 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
39 ovif ⊢ ( if ( 𝑣 = 𝑍 , 1 , 0 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = if ( 𝑣 = 𝑍 , ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) , ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) )
40 39 a1i ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( if ( 𝑣 = 𝑍 , 1 , 0 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = if ( 𝑣 = 𝑍 , ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) , ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) )
41 oveq2 ⊢ ( 𝑣 = 𝑍 → ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑍 ) )
42 41 adantl ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑣 = 𝑍 ) → ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑍 ) )
43 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
44 2 43 4 lmod1cl ⊢ ( 𝑀 ∈ LMod → 1 ∈ ( Base ‘ 𝑆 ) )
45 44 ancli ⊢ ( 𝑀 ∈ LMod → ( 𝑀 ∈ LMod ∧ 1 ∈ ( Base ‘ 𝑆 ) ) )
46 45 adantr ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 ∈ LMod ∧ 1 ∈ ( Base ‘ 𝑆 ) ) )
47 46 ad2antrr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑣 = 𝑍 ) → ( 𝑀 ∈ LMod ∧ 1 ∈ ( Base ‘ 𝑆 ) ) )
48 eqid ⊢ ( ·𝑠 ‘ 𝑀 ) = ( ·𝑠 ‘ 𝑀 )
49 2 48 43 5 lmodvs0 ⊢ ( ( 𝑀 ∈ LMod ∧ 1 ∈ ( Base ‘ 𝑆 ) ) → ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑍 ) = 𝑍 )
50 47 49 syl ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑣 = 𝑍 ) → ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑍 ) = 𝑍 )
51 42 50 eqtrd ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) ∧ 𝑣 = 𝑍 ) → ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
52 7 adantr ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑀 ∈ LMod )
53 elelpwi ⊢ ( ( 𝑣 ∈ 𝑉 ∧ 𝑉 ∈ 𝒫 𝐵 ) → 𝑣 ∈ 𝐵 )
54 53 expcom ⊢ ( 𝑉 ∈ 𝒫 𝐵 → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
55 54 adantl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑣 ∈ 𝑉 → 𝑣 ∈ 𝐵 ) )
56 55 imp ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝐵 )
57 1 2 48 3 5 lmod0vs ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑣 ∈ 𝐵 ) → ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
58 52 56 57 syl2anc ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
59 58 adantr ⊢ ( ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) ∧ ¬ 𝑣 = 𝑍 ) → ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
60 51 59 ifeqda ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → if ( 𝑣 = 𝑍 , ( 1 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) , ( 0 ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = 𝑍 )
61 38 40 60 3eqtrd ⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) = 𝑍 )
62 61 mpteq2dva ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) = ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) )
63 62 oveq2d ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ ( ( 𝐹 ‘ 𝑣 ) ( ·𝑠 ‘ 𝑀 ) 𝑣 ) ) ) = ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) ) )
64 lmodgrp ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
65 64 grpmndd ⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Mnd )
66 5 gsumz ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) ) = 𝑍 )
67 65 66 sylan ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝑀 Σg ( 𝑣 ∈ 𝑉 ↦ 𝑍 ) ) = 𝑍 )
68 29 63 67 3eqtrd ⊢ ( ( 𝑀 ∈ LMod ∧ 𝑉 ∈ 𝒫 𝐵 ) → ( 𝐹 ( linC ‘ 𝑀 ) 𝑉 ) = 𝑍 )