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 ( 1 ... ( 𝑛 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } )
Assertion	k0004val	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } )

Proof

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