Metamath Proof Explorer

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

Proof

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