Metamath Proof Explorer


Theorem lco0

Description: The set of empty linear combinations over a monoid is the singleton with the identity element of the monoid. (Contributed by AV, 12-Apr-2019)

Ref Expression
Assertion lco0 M Mnd M LinCo = 0 M

Proof

Step Hyp Ref Expression
1 0elpw 𝒫 Base M
2 eqid Base M = Base M
3 eqid Scalar M = Scalar M
4 eqid Base Scalar M = Base Scalar M
5 2 3 4 lcoop M Mnd 𝒫 Base M M LinCo = v Base M | w Base Scalar M finSupp 0 Scalar M w v = w linC M
6 1 5 mpan2 M Mnd M LinCo = v Base M | w Base Scalar M finSupp 0 Scalar M w v = w linC M
7 fvex Base Scalar M V
8 map0e Base Scalar M V Base Scalar M = 1 𝑜
9 7 8 mp1i M Mnd v Base M Base Scalar M = 1 𝑜
10 df1o2 1 𝑜 =
11 9 10 eqtrdi M Mnd v Base M Base Scalar M =
12 11 rexeqdv M Mnd v Base M w Base Scalar M finSupp 0 Scalar M w v = w linC M w finSupp 0 Scalar M w v = w linC M
13 lincval0 M Mnd linC M = 0 M
14 13 adantr M Mnd v Base M linC M = 0 M
15 14 eqeq2d M Mnd v Base M v = linC M v = 0 M
16 15 anbi2d M Mnd v Base M Fin v = linC M Fin v = 0 M
17 0ex V
18 breq1 w = finSupp 0 Scalar M w finSupp 0 Scalar M
19 fvex 0 Scalar M V
20 0fsupp 0 Scalar M V finSupp 0 Scalar M
21 19 20 ax-mp finSupp 0 Scalar M
22 0fin Fin
23 21 22 2th finSupp 0 Scalar M Fin
24 18 23 bitrdi w = finSupp 0 Scalar M w Fin
25 oveq1 w = w linC M = linC M
26 25 eqeq2d w = v = w linC M v = linC M
27 24 26 anbi12d w = finSupp 0 Scalar M w v = w linC M Fin v = linC M
28 27 rexsng V w finSupp 0 Scalar M w v = w linC M Fin v = linC M
29 17 28 mp1i M Mnd v Base M w finSupp 0 Scalar M w v = w linC M Fin v = linC M
30 22 a1i M Mnd v Base M Fin
31 30 biantrurd M Mnd v Base M v = 0 M Fin v = 0 M
32 16 29 31 3bitr4d M Mnd v Base M w finSupp 0 Scalar M w v = w linC M v = 0 M
33 12 32 bitrd M Mnd v Base M w Base Scalar M finSupp 0 Scalar M w v = w linC M v = 0 M
34 33 rabbidva M Mnd v Base M | w Base Scalar M finSupp 0 Scalar M w v = w linC M = v Base M | v = 0 M
35 eqid 0 M = 0 M
36 2 35 mndidcl M Mnd 0 M Base M
37 rabsn 0 M Base M v Base M | v = 0 M = 0 M
38 36 37 syl M Mnd v Base M | v = 0 M = 0 M
39 6 34 38 3eqtrd M Mnd M LinCo = 0 M