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 ( 0 ... 𝑛 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑡 ‘ 𝑘 ) = 1 } )
Assertion	k0004ss3	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) ⊆ ( Base ‘ ( 𝔼hil ‘ ( 𝑁 + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		k0004.a	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 𝑛 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑡 ‘ 𝑘 ) = 1 } )
2	1	k0004ss1	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) ⊆ ( ℝ ↑m ( 0 ... 𝑁 ) ) )
3		nn0z	⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
4		fzval3	⊢ ( 𝑁 ∈ ℤ → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
5	3 4	syl	⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... 𝑁 ) = ( 0 ..^ ( 𝑁 + 1 ) ) )
6	5	oveq2d	⊢ ( 𝑁 ∈ ℕ0 → ( ℝ ↑m ( 0 ... 𝑁 ) ) = ( ℝ ↑m ( 0 ..^ ( 𝑁 + 1 ) ) ) )
7		peano2nn0	⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
8		eqid	⊢ ( 𝔼hil ‘ ( 𝑁 + 1 ) ) = ( 𝔼hil ‘ ( 𝑁 + 1 ) )
9	8	ehlbase	⊢ ( ( 𝑁 + 1 ) ∈ ℕ0 → ( ℝ ↑m ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( Base ‘ ( 𝔼hil ‘ ( 𝑁 + 1 ) ) ) )
10	7 9	syl	⊢ ( 𝑁 ∈ ℕ0 → ( ℝ ↑m ( 0 ..^ ( 𝑁 + 1 ) ) ) = ( Base ‘ ( 𝔼hil ‘ ( 𝑁 + 1 ) ) ) )
11	6 10	eqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( ℝ ↑m ( 0 ... 𝑁 ) ) = ( Base ‘ ( 𝔼hil ‘ ( 𝑁 + 1 ) ) ) )
12	2 11	sseqtrd	⊢ ( 𝑁 ∈ ℕ0 → ( 𝐴 ‘ 𝑁 ) ⊆ ( Base ‘ ( 𝔼hil ‘ ( 𝑁 + 1 ) ) ) )