Metamath Proof Explorer

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 
|- A = ( n e. NN0 |-> { t e. ( ( 0 [,] 1 ) ^m ( 0 ... n ) ) | sum_ k e. ( 0 ... n ) ( t ` k ) = 1 } )
Assertion k0004ss3 
|- ( N e. NN0 -> ( A ` N ) C_ ( Base ` ( EEhil ` ( N + 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 k0004.a 
 |-  A = ( n e. NN0 |-> { t e. ( ( 0 [,] 1 ) ^m ( 0 ... n ) ) | sum_ k e. ( 0 ... n ) ( t ` k ) = 1 } )
2 1 k0004ss1 
 |-  ( N e. NN0 -> ( A ` N ) C_ ( RR ^m ( 0 ... N ) ) )
3 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
4 fzval3 
 |-  ( N e. ZZ -> ( 0 ... N ) = ( 0 ..^ ( N + 1 ) ) )
5 3 4 syl 
 |-  ( N e. NN0 -> ( 0 ... N ) = ( 0 ..^ ( N + 1 ) ) )
6 5 oveq2d 
 |-  ( N e. NN0 -> ( RR ^m ( 0 ... N ) ) = ( RR ^m ( 0 ..^ ( N + 1 ) ) ) )
7 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
8 eqid 
 |-  ( EEhil ` ( N + 1 ) ) = ( EEhil ` ( N + 1 ) )
9 8 ehlbase 
 |-  ( ( N + 1 ) e. NN0 -> ( RR ^m ( 0 ..^ ( N + 1 ) ) ) = ( Base ` ( EEhil ` ( N + 1 ) ) ) )
10 7 9 syl 
 |-  ( N e. NN0 -> ( RR ^m ( 0 ..^ ( N + 1 ) ) ) = ( Base ` ( EEhil ` ( N + 1 ) ) ) )
11 6 10 eqtrd 
 |-  ( N e. NN0 -> ( RR ^m ( 0 ... N ) ) = ( Base ` ( EEhil ` ( N + 1 ) ) ) )
12 2 11 sseqtrd 
 |-  ( N e. NN0 -> ( A ` N ) C_ ( Base ` ( EEhil ` ( N + 1 ) ) ) )