Theorem k0004ss1

Description: The topological simplex of dimension N is a subset of the real vectors 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	k0004ss1	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) ⊆ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		k0004.a	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑛 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } )
2	1	k0004val	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } )
3		simp2	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∧ Σ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 ) → 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑁 + 1 ) ) ) )
4	3	rabssdv	⊢ ( 𝑁 ∈ ℕ0 → { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } ⊆ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑁 + 1 ) ) ) )
5	2 4	eqsstrd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) ⊆ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑁 + 1 ) ) ) )
6		reex	⊢ ℝ ∈ V
7		unitssre	⊢ ( 0 [,] 1 ) ⊆ ℝ
8		mapss	⊢ ( ( ℝ ∈ V ∧ ( 0 [,] 1 ) ⊆ ℝ ) → ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ⊆ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) )
9	6 7 8	mp2an	⊢ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑁 + 1 ) ) ) ⊆ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) )
10	5 9	sstrdi	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) ⊆ ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) )