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 ⊢ B = Base M
linc0scn0.s ⊢ S = Scalar ⁡ M
linc0scn0.0 ⊢ 0 ˙ = 0 S
linc0scn0.1 ⊢ 1 ˙ = 1 S
linc0scn0.z ⊢ Z = 0 M
linc0scn0.f ⊢ F = x ∈ V ⟼ if x = Z 1 ˙ 0 ˙
Assertion linc0scn0 ⊢ M ∈ LMod ∧ V ∈ 𝒫 B → F linC ⁡ M V = Z

Proof

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