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 64 grpmndd M LMod M Mnd
66 5 gsumz M Mnd V 𝒫 B M v V Z = Z
67 65 66 sylan M LMod V 𝒫 B M v V Z = Z
68 29 63 67 3eqtrd M LMod V 𝒫 B F linC M V = Z