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

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	⊢ ( 𝜑 → 𝑆 ∈ ℕ₀ )
		reprf.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 ( repr ‘ 𝑆 ) 𝑀 ) )
	Assertion	reprf	⊢ ( 𝜑 → 𝐶 : ( 0 ..^ 𝑆 ) ⟶ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		reprval.a	⊢ ( 𝜑 → 𝐴 ⊆ ℕ )
2		reprval.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		reprval.s	⊢ ( 𝜑 → 𝑆 ∈ ℕ₀ )
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 ..^ 𝑆 ) ⟶ 𝐴 )