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	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑛 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } )
Assertion	k0004ss3	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) ⊆ ( Base ‘ ( 𝔼hil ‘ ( 𝑁 + 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		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
4		eqid	⊢ ( 𝔼hil ‘ ( 𝑁 + 1 ) ) = ( 𝔼hil ‘ ( 𝑁 + 1 ) )
5	4	ehlbase	⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) = ( Base ‘ ( 𝔼hil ‘ ( 𝑁 + 1 ) ) ) )
6	3 5	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ℝ ↑m ( 1 ... ( 𝑁 + 1 ) ) ) = ( Base ‘ ( 𝔼hil ‘ ( 𝑁 + 1 ) ) ) )
7	2 6	sseqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) ⊆ ( Base ‘ ( 𝔼hil ‘ ( 𝑁 + 1 ) ) ) )