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 ⊢ φ → A ⊆ ℕ
reprval.m ⊢ φ → M ∈ ℤ
reprval.s ⊢ φ → S ∈ ℕ 0
reprf.c ⊢ φ → C ∈ A repr ⁡ S M
Assertion reprf ⊢ φ → C : 0 ..^ S ⟶ A

Proof

Step Hyp Ref Expression
1 reprval.a ⊢ φ → A ⊆ ℕ
2 reprval.m ⊢ φ → M ∈ ℤ
3 reprval.s ⊢ φ → S ∈ ℕ 0
4 reprf.c ⊢ φ → C ∈ A repr ⁡ S M
5 1 2 3 reprval ⊢ φ → A repr ⁡ S M = c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
6 4 5 eleqtrd ⊢ φ → C ∈ c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M
7 elrabi ⊢ C ∈ c ∈ A 0 ..^ S | ∑ a ∈ 0 ..^ S c ⁡ a = M → C ∈ A 0 ..^ S
8 elmapi ⊢ C ∈ A 0 ..^ S → C : 0 ..^ S ⟶ A
9 6 7 8 3syl ⊢ φ → C : 0 ..^ S ⟶ A