Metamath Proof Explorer

Theorem k0004val0

Description: The topological simplex of dimension 0 is a singleton. (Contributed by RP, 2-Apr-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 k0004val0 
|- ( A ` 0 ) = { { <. 1 , 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 0nn0 
 |-  0 e. NN0
3 1 k0004val 
 |-  ( 0 e. NN0 -> ( A ` 0 ) = { t e. ( ( 0 [,] 1 ) ^m ( 1 ... ( 0 + 1 ) ) ) | sum_ k e. ( 1 ... ( 0 + 1 ) ) ( t ` k ) = 1 } )
4 2 3 ax-mp 
 |-  ( A ` 0 ) = { t e. ( ( 0 [,] 1 ) ^m ( 1 ... ( 0 + 1 ) ) ) | sum_ k e. ( 1 ... ( 0 + 1 ) ) ( t ` k ) = 1 }
5 0p1e1 
 |-  ( 0 + 1 ) = 1
6 5 oveq2i 
 |-  ( 1 ... ( 0 + 1 ) ) = ( 1 ... 1 )
7 1z 
 |-  1 e. ZZ
8 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
9 7 8 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
10 6 9 eqtri 
 |-  ( 1 ... ( 0 + 1 ) ) = { 1 }
11 10 oveq2i 
 |-  ( ( 0 [,] 1 ) ^m ( 1 ... ( 0 + 1 ) ) ) = ( ( 0 [,] 1 ) ^m { 1 } )
12 11 rabeqi 
 |-  { t e. ( ( 0 [,] 1 ) ^m ( 1 ... ( 0 + 1 ) ) ) | sum_ k e. ( 1 ... ( 0 + 1 ) ) ( t ` k ) = 1 } = { t e. ( ( 0 [,] 1 ) ^m { 1 } ) | sum_ k e. ( 1 ... ( 0 + 1 ) ) ( t ` k ) = 1 }
13 10 sumeq1i 
 |-  sum_ k e. ( 1 ... ( 0 + 1 ) ) ( t ` k ) = sum_ k e. { 1 } ( t ` k )
14 elmapi 
 |-  ( t e. ( ( 0 [,] 1 ) ^m { 1 } ) -> t : { 1 } --> ( 0 [,] 1 ) )
15 fsn2g 
 |-  ( 1 e. ZZ -> ( t : { 1 } --> ( 0 [,] 1 ) <-> ( ( t ` 1 ) e. ( 0 [,] 1 ) /\ t = { <. 1 , ( t ` 1 ) >. } ) ) )
16 7 15 ax-mp 
 |-  ( t : { 1 } --> ( 0 [,] 1 ) <-> ( ( t ` 1 ) e. ( 0 [,] 1 ) /\ t = { <. 1 , ( t ` 1 ) >. } ) )
17 16 biimpi 
 |-  ( t : { 1 } --> ( 0 [,] 1 ) -> ( ( t ` 1 ) e. ( 0 [,] 1 ) /\ t = { <. 1 , ( t ` 1 ) >. } ) )
18 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
19 ax-resscn 
 |-  RR C_ CC
20 18 19 sstri 
 |-  ( 0 [,] 1 ) C_ CC
21 20 sseli 
 |-  ( ( t ` 1 ) e. ( 0 [,] 1 ) -> ( t ` 1 ) e. CC )
22 21 adantr 
 |-  ( ( ( t ` 1 ) e. ( 0 [,] 1 ) /\ t = { <. 1 , ( t ` 1 ) >. } ) -> ( t ` 1 ) e. CC )
23 14 17 22 3syl 
 |-  ( t e. ( ( 0 [,] 1 ) ^m { 1 } ) -> ( t ` 1 ) e. CC )
24 fveq2 
 |-  ( k = 1 -> ( t ` k ) = ( t ` 1 ) )
25 24 sumsn 
 |-  ( ( 1 e. ZZ /\ ( t ` 1 ) e. CC ) -> sum_ k e. { 1 } ( t ` k ) = ( t ` 1 ) )
26 7 23 25 sylancr 
 |-  ( t e. ( ( 0 [,] 1 ) ^m { 1 } ) -> sum_ k e. { 1 } ( t ` k ) = ( t ` 1 ) )
27 13 26 syl5eq 
 |-  ( t e. ( ( 0 [,] 1 ) ^m { 1 } ) -> sum_ k e. ( 1 ... ( 0 + 1 ) ) ( t ` k ) = ( t ` 1 ) )
28 27 eqeq1d 
 |-  ( t e. ( ( 0 [,] 1 ) ^m { 1 } ) -> ( sum_ k e. ( 1 ... ( 0 + 1 ) ) ( t ` k ) = 1 <-> ( t ` 1 ) = 1 ) )
29 28 rabbiia 
 |-  { t e. ( ( 0 [,] 1 ) ^m { 1 } ) | sum_ k e. ( 1 ... ( 0 + 1 ) ) ( t ` k ) = 1 } = { t e. ( ( 0 [,] 1 ) ^m { 1 } ) | ( t ` 1 ) = 1 }
30 12 29 eqtri 
 |-  { t e. ( ( 0 [,] 1 ) ^m ( 1 ... ( 0 + 1 ) ) ) | sum_ k e. ( 1 ... ( 0 + 1 ) ) ( t ` k ) = 1 } = { t e. ( ( 0 [,] 1 ) ^m { 1 } ) | ( t ` 1 ) = 1 }
31 rabeqsn 
 |-  ( { t e. ( ( 0 [,] 1 ) ^m { 1 } ) | ( t ` 1 ) = 1 } = { { <. 1 , 1 >. } } <-> A. t ( ( t e. ( ( 0 [,] 1 ) ^m { 1 } ) /\ ( t ` 1 ) = 1 ) <-> t = { <. 1 , 1 >. } ) )
32 ovex 
 |-  ( 0 [,] 1 ) e. _V
33 1elunit 
 |-  1 e. ( 0 [,] 1 )
34 k0004lem3 
 |-  ( ( 1 e. ZZ /\ ( 0 [,] 1 ) e. _V /\ 1 e. ( 0 [,] 1 ) ) -> ( ( t e. ( ( 0 [,] 1 ) ^m { 1 } ) /\ ( t ` 1 ) = 1 ) <-> t = { <. 1 , 1 >. } ) )
35 7 32 33 34 mp3an 
 |-  ( ( t e. ( ( 0 [,] 1 ) ^m { 1 } ) /\ ( t ` 1 ) = 1 ) <-> t = { <. 1 , 1 >. } )
36 31 35 mpgbir 
 |-  { t e. ( ( 0 [,] 1 ) ^m { 1 } ) | ( t ` 1 ) = 1 } = { { <. 1 , 1 >. } }
37 30 36 eqtri 
 |-  { t e. ( ( 0 [,] 1 ) ^m ( 1 ... ( 0 + 1 ) ) ) | sum_ k e. ( 1 ... ( 0 + 1 ) ) ( t ` k ) = 1 } = { { <. 1 , 1 >. } }
38 4 37 eqtri 
 |-  ( A ` 0 ) = { { <. 1 , 1 >. } }