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	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑛 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } )
Assertion	k0004ss2	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) ⊆ ( Base ‘ ( ℝ^ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		k0004.a	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑛 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } )
2	1	k0004ss1	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) ⊆ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) )
3		ssidd	⊢ ( 𝑁 ∈ ℕ0 → ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ⊆ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) )
4		elmapi	⊢ ( 𝑣 ∈ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) → 𝑣 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ℝ )
5	4	adantl	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑣 ∈ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ) → 𝑣 : ( 1 ... ( 𝑁 + 1 ) ) ⟶ ℝ )
6		fzfid	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑣 ∈ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ) → ( 1 ... ( 𝑁 + 1 ) ) ∈ Fin )
7		0red	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑣 ∈ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ) → 0 ∈ ℝ )
8	5 6 7	fdmfifsupp	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑣 ∈ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ) → 𝑣 finSupp 0 )
9	3 8	ssrabdv	⊢ ( 𝑁 ∈ ℕ0 → ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ⊆ { 𝑣 ∈ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ 𝑣 finSupp 0 } )
10		ovex	⊢ ( 1 ... ( 𝑁 + 1 ) ) ∈ V
11		eqid	⊢ ( ℝ^ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) = ( ℝ^ ‘ ( 1 ... ( 𝑁 + 1 ) ) )
12		eqid	⊢ ( Base ‘ ( ℝ^ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ) = ( Base ‘ ( ℝ^ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) )
13	11 12	rrxbase	⊢ ( ( 1 ... ( 𝑁 + 1 ) ) ∈ V → ( Base ‘ ( ℝ^ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ) = { 𝑣 ∈ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ 𝑣 finSupp 0 } )
14	10 13	ax-mp	⊢ ( Base ‘ ( ℝ^ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ) = { 𝑣 ∈ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ 𝑣 finSupp 0 }
15	9 14	sseqtrrdi	⊢ ( 𝑁 ∈ ℕ0 → ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ⊆ ( Base ‘ ( ℝ^ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ) )
16	2 15	sstrd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) ⊆ ( Base ‘ ( ℝ^ ‘ ( 1 ... ( 𝑁 + 1 ) ) ) ) )