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 ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
reprval.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
reprval.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
reprf.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
Assertion reprsum ( 𝜑 → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝐶 ‘ 𝑎 ) = 𝑀 )

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
2 reprval.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 reprval.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4 reprf.c ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
5 1 2 3 reprval ⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
6 4 5 eleqtrd ⊢ ( 𝜑 → 𝐶 ∈ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
7 fveq1 ⊢ ( 𝑐 = 𝐶 → ( 𝑐 ‘ 𝑎 ) = ( 𝐶 ‘ 𝑎 ) )
8 7 sumeq2sdv ⊢ ( 𝑐 = 𝐶 → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝐶 ‘ 𝑎 ) )
9 8 eqeq1d ⊢ ( 𝑐 = 𝐶 → ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ↔ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝐶 ‘ 𝑎 ) = 𝑀 ) )
10 9 elrab ⊢ ( 𝐶 ∈ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ↔ ( 𝐶 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝐶 ‘ 𝑎 ) = 𝑀 ) )
11 6 10 sylib ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∧ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝐶 ‘ 𝑎 ) = 𝑀 ) )
12 11 simprd ⊢ ( 𝜑 → Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝐶 ‘ 𝑎 ) = 𝑀 )