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 | |
|
Assertion | k0004val | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | k0004.a | |
|
2 | oveq1 | |
|
3 | 2 | oveq2d | |
4 | 3 | oveq2d | |
5 | 3 | sumeq1d | |
6 | 5 | eqeq1d | |
7 | 4 6 | rabeqbidv | |
8 | ovex | |
|
9 | 8 | rabex | |
10 | 7 1 9 | fvmpt | |