Metamath Proof Explorer

Theorem k0004ss2

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

		Ref	Expression
	Hypothesis	k0004.a	$⊢ A = (n \in ℕ_{0} ⟼ \{t \in ({[0, 1]}^{(0 \dots n)}) \| \sum_{k = 0}^{n} t (k) = 1\})$
	Assertion	k0004ss2	$⊢ N \in ℕ_{0} \to A (N) \subseteq {Base}_{(0 \dots N)}$

Proof

Step	Hyp	Ref	Expression
1		k0004.a	$⊢ A = (n \in ℕ_{0} ⟼ \{t \in ({[0, 1]}^{(0 \dots n)}) \| \sum_{k = 0}^{n} t (k) = 1\})$
2	1	k0004ss1	$⊢ N \in ℕ_{0} \to A (N) \subseteq ℝ^{(0 \dots N)}$
3		ssidd	$⊢ N \in ℕ_{0} \to ℝ^{(0 \dots N)} \subseteq ℝ^{(0 \dots N)}$
4		elmapi	$⊢ v \in (ℝ^{(0 \dots N)}) \to v : (0 \dots N) ⟶ ℝ$
5	4	adantl	$⊢ (N \in ℕ_{0} \land v \in (ℝ^{(0 \dots N)})) \to v : (0 \dots N) ⟶ ℝ$
6		fzfid	$⊢ (N \in ℕ_{0} \land v \in (ℝ^{(0 \dots N)})) \to (0 \dots N) \in Fin$
7		0red	$⊢ (N \in ℕ_{0} \land v \in (ℝ^{(0 \dots N)})) \to 0 \in ℝ$
8	5 6 7	fdmfifsupp	$⊢ (N \in ℕ_{0} \land v \in (ℝ^{(0 \dots N)})) \to {finSupp}_{0} (v)$
9	3 8	ssrabdv	$⊢ N \in ℕ_{0} \to ℝ^{(0 \dots N)} \subseteq \{v \in (ℝ^{(0 \dots N)}) \| {finSupp}_{0} (v)\}$
10		ovex	$⊢ (0 \dots N) \in V$
11		eqid	$⊢ (0 \dots N) = (0 \dots N)$
12		eqid	$⊢ {Base}_{(0 \dots N)} = {Base}_{(0 \dots N)}$
13	11 12	rrxbase	$⊢ (0 \dots N) \in V \to {Base}_{(0 \dots N)} = \{v \in (ℝ^{(0 \dots N)}) \| {finSupp}_{0} (v)\}$
14	10 13	ax-mp	$⊢ {Base}_{(0 \dots N)} = \{v \in (ℝ^{(0 \dots N)}) \| {finSupp}_{0} (v)\}$
15	9 14	sseqtrrdi	$⊢ N \in ℕ_{0} \to ℝ^{(0 \dots N)} \subseteq {Base}_{(0 \dots N)}$
16	2 15	sstrd	$⊢ N \in ℕ_{0} \to A (N) \subseteq {Base}_{(0 \dots N)}$