Metamath Proof Explorer


Theorem reprf

Description: Members of the representation of M as the sum of S nonnegative integers from set A as functions. (Contributed by Thierry Arnoux, 5-Dec-2021)

Ref Expression
Hypotheses reprval.a ( 𝜑𝐴 ⊆ ℕ )
reprval.m ( 𝜑𝑀 ∈ ℤ )
reprval.s ( 𝜑𝑆 ∈ ℕ0 )
reprf.c ( 𝜑𝐶 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
Assertion reprf ( 𝜑𝐶 : ( 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 elrabi ( 𝐶 ∈ { 𝑐 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐𝑎 ) = 𝑀 } → 𝐶 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) )
8 elmapi ( 𝐶 ∈ ( 𝐴m ( 0 ..^ 𝑆 ) ) → 𝐶 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )
9 6 7 8 3syl ( 𝜑𝐶 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )