Theorem reprval

Description: Value of the representations of M as the sum of S nonnegative integers in a given set A . (Contributed by Thierry Arnoux, 1-Dec-2021)

	Ref	Expression
Hypotheses	reprval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
	reprval.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	reprval.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
Assertion	reprval	⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )

Proof

Step	Hyp	Ref	Expression
1		reprval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
2		reprval.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		reprval.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
4		df-repr	⊢ repr = ( 𝑠 ∈ ℕ0 ↦ ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) )
5		oveq2	⊢ ( 𝑠 = 𝑆 → ( 0 ..^ 𝑠 ) = ( 0 ..^ 𝑆 ) )
6	5	oveq2d	⊢ ( 𝑠 = 𝑆 → ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) = ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) )
7	5	sumeq1d	⊢ ( 𝑠 = 𝑆 → Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) )
8	7	eqeq1d	⊢ ( 𝑠 = 𝑆 → ( Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 ↔ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 ) )
9	6 8	rabeqbidv	⊢ ( 𝑠 = 𝑆 → { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } = { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } )
10	9	mpoeq3dv	⊢ ( 𝑠 = 𝑆 → ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑠 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑠 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) = ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) )
11		nnex	⊢ ℕ ∈ V
12	11	pwex	⊢ 𝒫 ℕ ∈ V
13		zex	⊢ ℤ ∈ V
14	12 13	mpoex	⊢ ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) ∈ V
15	14	a1i	⊢ ( 𝜑 → ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) ∈ V )
16	4 10 3 15	fvmptd3	⊢ ( 𝜑 → ( repr ‘ 𝑆 ) = ( 𝑏 ∈ 𝒫 ℕ , 𝑚 ∈ ℤ ↦ { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } ) )
17		simprl	⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝐴 ∧ 𝑚 = 𝑀 ) ) → 𝑏 = 𝐴 )
18	17	oveq1d	⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝐴 ∧ 𝑚 = 𝑀 ) ) → ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) = ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) )
19		simprr	⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝐴 ∧ 𝑚 = 𝑀 ) ) → 𝑚 = 𝑀 )
20	19	eqeq2d	⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝐴 ∧ 𝑚 = 𝑀 ) ) → ( Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 ↔ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 ) )
21	18 20	rabeqbidv	⊢ ( ( 𝜑 ∧ ( 𝑏 = 𝐴 ∧ 𝑚 = 𝑀 ) ) → { 𝑐 ∈ ( 𝑏 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑚 } = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )
22	11	a1i	⊢ ( 𝜑 → ℕ ∈ V )
23	22 1	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
24	23 1	elpwd	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 ℕ )
25		ovex	⊢ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∈ V
26	25	rabex	⊢ { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ∈ V
27	26	a1i	⊢ ( 𝜑 → { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } ∈ V )
28	16 21 24 2 27	ovmpod	⊢ ( 𝜑 → ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) = { 𝑐 ∈ ( 𝐴 ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = 𝑀 } )