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→MLinCo∅=0M

Proof

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