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 ( 1 ... ( n + 1 ) ) ) | sum_ k e. ( 1 ... ( n + 1 ) ) ( 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 ( 1 ... ( n + 1 ) ) ) | sum_ k e. ( 1 ... ( n + 1 ) ) ( t ` k ) = 1 } )
2 1 k0004ss1 
 |-  ( N e. NN0 -> ( A ` N ) C_ ( RR ^m ( 1 ... ( N + 1 ) ) ) )
3 peano2nn0 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN0 )
4 eqid 
 |-  ( EEhil ` ( N + 1 ) ) = ( EEhil ` ( N + 1 ) )
5 4 ehlbase 
 |-  ( ( N + 1 ) e. NN0 -> ( RR ^m ( 1 ... ( N + 1 ) ) ) = ( Base ` ( EEhil ` ( N + 1 ) ) ) )
6 3 5 syl 
 |-  ( N e. NN0 -> ( RR ^m ( 1 ... ( N + 1 ) ) ) = ( Base ` ( EEhil ` ( N + 1 ) ) ) )
7 2 6 sseqtrd 
 |-  ( N e. NN0 -> ( A ` N ) C_ ( Base ` ( EEhil ` ( N + 1 ) ) ) )