Theorem k0004ss1

Description: The topological simplex of dimension N is a subset of the real vectors of dimension ( N + 1 ) . (Contributed by RP, 29-Mar-2021)

	Ref	Expression
Hypothesis	k0004.a	$$⊢A=\left(n\in {\mathbb{N}}_0⟼\left\{t\in \left({\left[0,1\right]}^{\left(1\dots n+1\right)}\right)|\sum _{k=1}^{n+1}t\left(k\right)=1\right\}\right)$$
Assertion	k0004ss1	$$⊢N\in {\mathbb{N}}_0\to A\left(N\right)\subseteq {ℝ}^{\left(1\dots N+1\right)}$$

Proof

Step	Hyp	Ref	Expression
1		k0004.a	$$⊢A=\left(n\in {\mathbb{N}}_0⟼\left\{t\in \left({\left[0,1\right]}^{\left(1\dots n+1\right)}\right)|\sum _{k=1}^{n+1}t\left(k\right)=1\right\}\right)$$
2	1	k0004val	$$⊢N\in {\mathbb{N}}_0\to A\left(N\right)=\left\{t\in \left({\left[0,1\right]}^{\left(1\dots N+1\right)}\right)|\sum _{k=1}^{N+1}t\left(k\right)=1\right\}$$
3		simp2	$$⊢\left(N\in {\mathbb{N}}_0\wedge t\in \left({\left[0,1\right]}^{\left(1\dots N+1\right)}\right)\wedge \sum _{k=1}^{N+1}t\left(k\right)=1\right)\to t\in \left({\left[0,1\right]}^{\left(1\dots N+1\right)}\right)$$
4	3	rabssdv	$$⊢N\in {\mathbb{N}}_0\to \left\{t\in \left({\left[0,1\right]}^{\left(1\dots N+1\right)}\right)|\sum _{k=1}^{N+1}t\left(k\right)=1\right\}\subseteq {\left[0,1\right]}^{\left(1\dots N+1\right)}$$
5	2 4	eqsstrd	$$⊢N\in {\mathbb{N}}_0\to A\left(N\right)\subseteq {\left[0,1\right]}^{\left(1\dots N+1\right)}$$
6		reex	$$⊢ℝ\in \mathrm{V}$$
7		unitssre	$$⊢\left[0,1\right]\subseteq ℝ$$
8		mapss	$$⊢\left(ℝ\in \mathrm{V}\wedge \left[0,1\right]\subseteq ℝ\right)\to {\left[0,1\right]}^{\left(1\dots N+1\right)}\subseteq {ℝ}^{\left(1\dots N+1\right)}$$
9	6 7 8	mp2an	$$⊢{\left[0,1\right]}^{\left(1\dots N+1\right)}\subseteq {ℝ}^{\left(1\dots N+1\right)}$$
10	5 9	sstrdi	$$⊢N\in {\mathbb{N}}_0\to A\left(N\right)\subseteq {ℝ}^{\left(1\dots N+1\right)}$$