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 0fi ⊢ ∅ ∈ 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