Metamath Proof Explorer

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 
|- A = ( n e. NN0 |-> { t e. ( ( 0 [,] 1 ) ^m ( 1 ... ( n + 1 ) ) ) | sum_ k e. ( 1 ... ( n + 1 ) ) ( t ` k ) = 1 } )
Assertion k0004ss1 
|- ( N e. NN0 -> ( A ` N ) C_ ( RR ^m ( 1 ... ( 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 k0004val 
 |-  ( N e. NN0 -> ( A ` N ) = { t e. ( ( 0 [,] 1 ) ^m ( 1 ... ( N + 1 ) ) ) | sum_ k e. ( 1 ... ( N + 1 ) ) ( t ` k ) = 1 } )
3 simp2 
 |-  ( ( N e. NN0 /\ t e. ( ( 0 [,] 1 ) ^m ( 1 ... ( N + 1 ) ) ) /\ sum_ k e. ( 1 ... ( N + 1 ) ) ( t ` k ) = 1 ) -> t e. ( ( 0 [,] 1 ) ^m ( 1 ... ( N + 1 ) ) ) )
4 3 rabssdv 
 |-  ( N e. NN0 -> { t e. ( ( 0 [,] 1 ) ^m ( 1 ... ( N + 1 ) ) ) | sum_ k e. ( 1 ... ( N + 1 ) ) ( t ` k ) = 1 } C_ ( ( 0 [,] 1 ) ^m ( 1 ... ( N + 1 ) ) ) )
5 2 4 eqsstrd 
 |-  ( N e. NN0 -> ( A ` N ) C_ ( ( 0 [,] 1 ) ^m ( 1 ... ( N + 1 ) ) ) )
6 reex 
 |-  RR e. _V
7 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
8 mapss 
 |-  ( ( RR e. _V /\ ( 0 [,] 1 ) C_ RR ) -> ( ( 0 [,] 1 ) ^m ( 1 ... ( N + 1 ) ) ) C_ ( RR ^m ( 1 ... ( N + 1 ) ) ) )
9 6 7 8 mp2an 
 |-  ( ( 0 [,] 1 ) ^m ( 1 ... ( N + 1 ) ) ) C_ ( RR ^m ( 1 ... ( N + 1 ) ) )
10 5 9 sstrdi 
 |-  ( N e. NN0 -> ( A ` N ) C_ ( RR ^m ( 1 ... ( N + 1 ) ) ) )