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	|- A = ( n e. NN0 |-> { t e. ( ( 0 [,] 1 ) ^m ( 0 ... n ) ) | sum_ k e. ( 0 ... n ) ( t ` k ) = 1 } )
Assertion	k0004val	|- ( N e. NN0 -> ( A ` N ) = { t e. ( ( 0 [,] 1 ) ^m ( 0 ... N ) ) | sum_ k e. ( 0 ... N ) ( t ` k ) = 1 } )

Proof

Step	Hyp	Ref	Expression
1		k0004.a	|- A = ( n e. NN0 |-> { t e. ( ( 0 [,] 1 ) ^m ( 0 ... n ) ) | sum_ k e. ( 0 ... n ) ( t ` k ) = 1 } )
2		oveq2	|- ( n = N -> ( 0 ... n ) = ( 0 ... N ) )
3	2	oveq2d	|- ( n = N -> ( ( 0 [,] 1 ) ^m ( 0 ... n ) ) = ( ( 0 [,] 1 ) ^m ( 0 ... N ) ) )
4	2	sumeq1d	|- ( n = N -> sum_ k e. ( 0 ... n ) ( t ` k ) = sum_ k e. ( 0 ... N ) ( t ` k ) )
5	4	eqeq1d	|- ( n = N -> ( sum_ k e. ( 0 ... n ) ( t ` k ) = 1 <-> sum_ k e. ( 0 ... N ) ( t ` k ) = 1 ) )
6	3 5	rabeqbidv	|- ( n = N -> { t e. ( ( 0 [,] 1 ) ^m ( 0 ... n ) ) | sum_ k e. ( 0 ... n ) ( t ` k ) = 1 } = { t e. ( ( 0 [,] 1 ) ^m ( 0 ... N ) ) | sum_ k e. ( 0 ... N ) ( t ` k ) = 1 } )
7		ovex	|- ( ( 0 [,] 1 ) ^m ( 0 ... N ) ) e. _V
8	7	rabex	|- { t e. ( ( 0 [,] 1 ) ^m ( 0 ... N ) ) | sum_ k e. ( 0 ... N ) ( t ` k ) = 1 } e. _V
9	6 1 8	fvmpt	|- ( N e. NN0 -> ( A ` N ) = { t e. ( ( 0 [,] 1 ) ^m ( 0 ... N ) ) | sum_ k e. ( 0 ... N ) ( t ` k ) = 1 } )