Theorem k0004val

Description: The topological simplex of dimension N is the set of real vectors where the components are nonnegative and sum to 1. (Contributed by RP, 29-Mar-2021)

	Ref	Expression
Hypothesis	k0004.a	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 𝑛 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑡 ‘ 𝑘 ) = 1 } )
Assertion	k0004val	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 𝑁 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑡 ‘ 𝑘 ) = 1 } )

Proof

Step	Hyp	Ref	Expression
1		k0004.a	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 𝑛 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑡 ‘ 𝑘 ) = 1 } )
2		oveq2	⊢ ( 𝑛 = 𝑁 → ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) )
3	2	oveq2d	⊢ ( 𝑛 = 𝑁 → ( ( 0 [,] 1 ) ↑m ( 0 ... 𝑛 ) ) = ( ( 0 [,] 1 ) ↑m ( 0 ... 𝑁 ) ) )
4	2	sumeq1d	⊢ ( 𝑛 = 𝑁 → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑡 ‘ 𝑘 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑡 ‘ 𝑘 ) )
5	4	eqeq1d	⊢ ( 𝑛 = 𝑁 → ( Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑡 ‘ 𝑘 ) = 1 ↔ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑡 ‘ 𝑘 ) = 1 ) )
6	3 5	rabeqbidv	⊢ ( 𝑛 = 𝑁 → { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 𝑛 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑡 ‘ 𝑘 ) = 1 } = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 𝑁 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑡 ‘ 𝑘 ) = 1 } )
7		ovex	⊢ ( ( 0 [,] 1 ) ↑m ( 0 ... 𝑁 ) ) ∈ V
8	7	rabex	⊢ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 𝑁 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑡 ‘ 𝑘 ) = 1 } ∈ V
9	6 1 8	fvmpt	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 𝑁 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑡 ‘ 𝑘 ) = 1 } )