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]}^{(1 \dots n + 1)}) \| \sum_{k = 1}^{n + 1} t (k) = 1\})$
	Assertion	k0004ss2	$⊢ N \in ℕ_{0} \to A (N) \subseteq {Base}_{msup}$

Proof

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