Theorem k0004ss3

Description: The topological simplex of dimension N is a subset of the base set of Euclidean space 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	k0004ss3	$$⊢N\in {\mathbb{N}}_0\to A\left(N\right)\subseteq {\mathrm{Base}}_{{𝔼}_{\mathrm{hil}}\left(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	k0004ss1	$$⊢N\in {\mathbb{N}}_0\to A\left(N\right)\subseteq {ℝ}^{\left(1\dots N+1\right)}$$
3		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
4		eqid	$$⊢{𝔼}_{\mathrm{hil}}\left(N+1\right)={𝔼}_{\mathrm{hil}}\left(N+1\right)$$
5	4	ehlbase	$$⊢N+1\in {\mathbb{N}}_0\to {ℝ}^{\left(1\dots N+1\right)}={\mathrm{Base}}_{{𝔼}_{\mathrm{hil}}\left(N+1\right)}$$
6	3 5	syl	$$⊢N\in {\mathbb{N}}_0\to {ℝ}^{\left(1\dots N+1\right)}={\mathrm{Base}}_{{𝔼}_{\mathrm{hil}}\left(N+1\right)}$$
7	2 6	sseqtrd	$$⊢N\in {\mathbb{N}}_0\to A\left(N\right)\subseteq {\mathrm{Base}}_{{𝔼}_{\mathrm{hil}}\left(N+1\right)}$$