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=n0t011n+1|k=1n+1tk=1
Assertion k0004val N0AN=t011N+1|k=1N+1tk=1

Proof

Step Hyp Ref Expression
1 k0004.a A=n0t011n+1|k=1n+1tk=1
2 oveq1 n=Nn+1=N+1
3 2 oveq2d n=N1n+1=1N+1
4 3 oveq2d n=N011n+1=011N+1
5 3 sumeq1d n=Nk=1n+1tk=k=1N+1tk
6 5 eqeq1d n=Nk=1n+1tk=1k=1N+1tk=1
7 4 6 rabeqbidv n=Nt011n+1|k=1n+1tk=1=t011N+1|k=1N+1tk=1
8 ovex 011N+1V
9 8 rabex t011N+1|k=1N+1tk=1V
10 7 1 9 fvmpt N0AN=t011N+1|k=1N+1tk=1