Metamath Proof Explorer

Theorem repr0

Description: There is exactly one representation with no elements (an empty sum), only for M = 0 . (Contributed by Thierry Arnoux, 2-Dec-2021)

Ref Expression
Hypotheses reprval.a ⊢φ→A⊆ℕ
reprval.m ⊢φ→M∈ℤ
reprval.s ⊢φ→S∈ℕ0
Assertion repr0 ⊢φ→Arepr⁡0M=ifM=0∅∅

Proof

Step Hyp Ref Expression
1 reprval.a ⊢φ→A⊆ℕ
2 reprval.m ⊢φ→M∈ℤ
3 reprval.s ⊢φ→S∈ℕ0
4 0nn0 ⊢0∈ℕ0
5 4 a1i ⊢φ→0∈ℕ0
6 1 2 5 reprval ⊢φ→Arepr⁡0M=c∈A0..^0|∑a∈0..^0c⁡a=M
7 fzo0 ⊢0..^0=∅
8 7 sumeq1i ⊢∑a∈0..^0c⁡a=∑a∈∅c⁡a
9 sum0 ⊢∑a∈∅c⁡a=0
10 8 9 eqtri ⊢∑a∈0..^0c⁡a=0
11 10 eqeq1i ⊢∑a∈0..^0c⁡a=M↔0=M
12 11 a1i ⊢c=∅→∑a∈0..^0c⁡a=M↔0=M
13 0ex ⊢∅∈V
14 13 snid ⊢∅∈∅
15 nnex ⊢ℕ∈V
16 15 a1i ⊢φ→ℕ∈V
17 16 1 ssexd ⊢φ→A∈V
18 mapdm0 ⊢A∈V→A∅=∅
19 17 18 syl ⊢φ→A∅=∅
20 14 19 eleqtrrid ⊢φ→∅∈A∅
21 7 oveq2i ⊢A0..^0=A∅
22 20 21 eleqtrrdi ⊢φ→∅∈A0..^0
23 22 adantr ⊢φ∧M=0→∅∈A0..^0
24 simpr ⊢φ∧M=0→M=0
25 24 eqcomd ⊢φ∧M=0→0=M
26 21 19 eqtrid ⊢φ→A0..^0=∅
27 26 eleq2d ⊢φ→c∈A0..^0↔c∈∅
28 27 biimpa ⊢φ∧c∈A0..^0→c∈∅
29 elsni ⊢c∈∅→c=∅
30 28 29 syl ⊢φ∧c∈A0..^0→c=∅
31 30 ad4ant13 ⊢φ∧M=0∧c∈A0..^0∧∑a∈0..^0c⁡a=M→c=∅
32 12 23 25 31 rabeqsnd ⊢φ∧M=0→c∈A0..^0|∑a∈0..^0c⁡a=M=∅
33 32 eqcomd ⊢φ∧M=0→∅=c∈A0..^0|∑a∈0..^0c⁡a=M
34 10 a1i ⊢φ∧¬M=0∧c∈A0..^0→∑a∈0..^0c⁡a=0
35 simplr ⊢φ∧¬M=0∧c∈A0..^0→¬M=0
36 35 neqned ⊢φ∧¬M=0∧c∈A0..^0→M≠0
37 36 necomd ⊢φ∧¬M=0∧c∈A0..^0→0≠M
38 34 37 eqnetrd ⊢φ∧¬M=0∧c∈A0..^0→∑a∈0..^0c⁡a≠M
39 38 neneqd ⊢φ∧¬M=0∧c∈A0..^0→¬∑a∈0..^0c⁡a=M
40 39 ralrimiva ⊢φ∧¬M=0→∀c∈A0..^0¬∑a∈0..^0c⁡a=M
41 rabeq0 ⊢c∈A0..^0|∑a∈0..^0c⁡a=M=∅↔∀c∈A0..^0¬∑a∈0..^0c⁡a=M
42 40 41 sylibr ⊢φ∧¬M=0→c∈A0..^0|∑a∈0..^0c⁡a=M=∅
43 42 eqcomd ⊢φ∧¬M=0→∅=c∈A0..^0|∑a∈0..^0c⁡a=M
44 33 43 ifeqda ⊢φ→ifM=0∅∅=c∈A0..^0|∑a∈0..^0c⁡a=M
45 6 44 eqtr4d ⊢φ→Arepr⁡0M=ifM=0∅∅