Theorem k0004ss2

Description: The topological simplex of dimension N is a subset of the base set of a real vector 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	k0004ss2	|- ( N e. NN0 -> ( A ` N ) C_ ( Base ` ( RR^ ` ( 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	k0004ss1	|- ( N e. NN0 -> ( A ` N ) C_ ( RR ^m ( 1 ... ( N + 1 ) ) ) )
3		ssidd	|- ( N e. NN0 -> ( RR ^m ( 1 ... ( N + 1 ) ) ) C_ ( RR ^m ( 1 ... ( N + 1 ) ) ) )
4		elmapi	|- ( v e. ( RR ^m ( 1 ... ( N + 1 ) ) ) -> v : ( 1 ... ( N + 1 ) ) --> RR )
5	4	adantl	|- ( ( N e. NN0 /\ v e. ( RR ^m ( 1 ... ( N + 1 ) ) ) ) -> v : ( 1 ... ( N + 1 ) ) --> RR )
6		fzfid	|- ( ( N e. NN0 /\ v e. ( RR ^m ( 1 ... ( N + 1 ) ) ) ) -> ( 1 ... ( N + 1 ) ) e. Fin )
7		0red	|- ( ( N e. NN0 /\ v e. ( RR ^m ( 1 ... ( N + 1 ) ) ) ) -> 0 e. RR )
8	5 6 7	fdmfifsupp	|- ( ( N e. NN0 /\ v e. ( RR ^m ( 1 ... ( N + 1 ) ) ) ) -> v finSupp 0 )
9	3 8	ssrabdv	|- ( N e. NN0 -> ( RR ^m ( 1 ... ( N + 1 ) ) ) C_ { v e. ( RR ^m ( 1 ... ( N + 1 ) ) ) | v finSupp 0 } )
10		ovex	|- ( 1 ... ( N + 1 ) ) e. _V
11		eqid	|- ( RR^ ` ( 1 ... ( N + 1 ) ) ) = ( RR^ ` ( 1 ... ( N + 1 ) ) )
12		eqid	|- ( Base ` ( RR^ ` ( 1 ... ( N + 1 ) ) ) ) = ( Base ` ( RR^ ` ( 1 ... ( N + 1 ) ) ) )
13	11 12	rrxbase	|- ( ( 1 ... ( N + 1 ) ) e. _V -> ( Base ` ( RR^ ` ( 1 ... ( N + 1 ) ) ) ) = { v e. ( RR ^m ( 1 ... ( N + 1 ) ) ) | v finSupp 0 } )
14	10 13	ax-mp	|- ( Base ` ( RR^ ` ( 1 ... ( N + 1 ) ) ) ) = { v e. ( RR ^m ( 1 ... ( N + 1 ) ) ) | v finSupp 0 }
15	9 14	sseqtrrdi	|- ( N e. NN0 -> ( RR ^m ( 1 ... ( N + 1 ) ) ) C_ ( Base ` ( RR^ ` ( 1 ... ( N + 1 ) ) ) ) )
16	2 15	sstrd	|- ( N e. NN0 -> ( A ` N ) C_ ( Base ` ( RR^ ` ( 1 ... ( N + 1 ) ) ) ) )