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 ..^ 𝑆 ) ( 𝐶 ‘ 𝑎 ) = 𝑀 )