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

Metamath Proof Explorer

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