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(0\dots n\right)}\right)|\sum _{k=0}^{n}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(0\dots n\right)}\right)|\sum _{k=0}^{n}t\left(k\right)=1\right\}\right)$$
2	1	k0004ss1	$$⊢N\in {\mathbb{N}}_0\to A\left(N\right)\subseteq {ℝ}^{\left(0\dots N\right)}$$
3		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
4		fzval3	$$⊢N\in \mathbb{Z}\to \left(0\dots N\right)=\left(0..^N+1\right)$$
5	3 4	syl	$$⊢N\in {\mathbb{N}}_0\to \left(0\dots N\right)=\left(0..^N+1\right)$$
6	5	oveq2d	$$⊢N\in {\mathbb{N}}_0\to {ℝ}^{\left(0\dots N\right)}={ℝ}^{\left(0..^N+1\right)}$$
7		peano2nn0	$$⊢N\in {\mathbb{N}}_0\to N+1\in {\mathbb{N}}_0$$
8		eqid	$$⊢{𝔼}_{\mathrm{hil}}\left(N+1\right)={𝔼}_{\mathrm{hil}}\left(N+1\right)$$
9	8	ehlbase	$$⊢N+1\in {\mathbb{N}}_0\to {ℝ}^{\left(0..^N+1\right)}={\mathrm{Base}}_{{𝔼}_{\mathrm{hil}}\left(N+1\right)}$$
10	7 9	syl	$$⊢N\in {\mathbb{N}}_0\to {ℝ}^{\left(0..^N+1\right)}={\mathrm{Base}}_{{𝔼}_{\mathrm{hil}}\left(N+1\right)}$$
11	6 10	eqtrd	$$⊢N\in {\mathbb{N}}_0\to {ℝ}^{\left(0\dots N\right)}={\mathrm{Base}}_{{𝔼}_{\mathrm{hil}}\left(N+1\right)}$$
12	2 11	sseqtrd	$$⊢N\in {\mathbb{N}}_0\to A\left(N\right)\subseteq {\mathrm{Base}}_{{𝔼}_{\mathrm{hil}}\left(N+1\right)}$$