This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem reprsum

Description: Sums of values of the members of the representation of M equal M . (Contributed by Thierry Arnoux, 5-Dec-2021)

Ref Expression
Hypotheses reprval.a ⊢ φ → A ⊆ ℕ
reprval.m ⊢ φ → M ∈ ℤ
reprval.s ⊢ φ → S ∈ ℕ 0
reprf.c ⊢ φ → C ∈ A repr ⁡ S M
Assertion reprsum ⊢ φ → ∑ a ∈ 0 ..^ S C ⁡ a = M

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ φ → A ⊆ ℕ
2 reprval.m ⊢ φ → M ∈ ℤ
3 reprval.s ⊢ φ → S ∈ ℕ 0
4 reprf.c ⊢ φ → C ∈ A repr ⁡ S M
5 1 2 3 reprval ⊢ φ → A repr ⁡ S M = c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
6 4 5 eleqtrd ⊢ φ → C ∈ c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
7 fveq1 ⊢ c = C → c ⁡ a = C ⁡ a
8 7 sumeq2sdv ⊢ c = C → ∑ a ∈ 0 ..^ S c ⁡ a = ∑ a ∈ 0 ..^ S C ⁡ a
9 8 eqeq1d ⊢ c = C → ∑ a ∈ 0 ..^ S c ⁡ a = M ↔ ∑ a ∈ 0 ..^ S C ⁡ a = M
10 9 elrab ⊢ C ∈ c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M ↔ C ∈ A 0 ..^ S ∧ ∑ a ∈ 0 ..^ S C ⁡ a = M
11 6 10 sylib ⊢ φ → C ∈ A 0 ..^ S ∧ ∑ a ∈ 0 ..^ S C ⁡ a = M
12 11 simprd ⊢ φ → ∑ a ∈ 0 ..^ S C ⁡ a = M