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 ( 0 ... n ) ) | sum_ k e. ( 0 ... n ) ( t ` k ) = 1 } )
Assertion k0004val0 
|- ( A ` 0 ) = { <" 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 fz0sn 
 |-  ( 0 ... 0 ) = { 0 }
3 2 oveq2i 
 |-  ( ( 0 [,] 1 ) ^m ( 0 ... 0 ) ) = ( ( 0 [,] 1 ) ^m { 0 } )
4 3 rabeqi 
 |-  { t e. ( ( 0 [,] 1 ) ^m ( 0 ... 0 ) ) | sum_ k e. ( 0 ... 0 ) ( t ` k ) = 1 } = { t e. ( ( 0 [,] 1 ) ^m { 0 } ) | sum_ k e. ( 0 ... 0 ) ( t ` k ) = 1 }
5 2 sumeq1i 
 |-  sum_ k e. ( 0 ... 0 ) ( t ` k ) = sum_ k e. { 0 } ( t ` k )
6 0z 
 |-  0 e. ZZ
7 elmapi 
 |-  ( t e. ( ( 0 [,] 1 ) ^m { 0 } ) -> t : { 0 } --> ( 0 [,] 1 ) )
8 fsn2g 
 |-  ( 0 e. ZZ -> ( t : { 0 } --> ( 0 [,] 1 ) <-> ( ( t ` 0 ) e. ( 0 [,] 1 ) /\ t = { <. 0 , ( t ` 0 ) >. } ) ) )
9 6 8 ax-mp 
 |-  ( t : { 0 } --> ( 0 [,] 1 ) <-> ( ( t ` 0 ) e. ( 0 [,] 1 ) /\ t = { <. 0 , ( t ` 0 ) >. } ) )
10 9 biimpi 
 |-  ( t : { 0 } --> ( 0 [,] 1 ) -> ( ( t ` 0 ) e. ( 0 [,] 1 ) /\ t = { <. 0 , ( t ` 0 ) >. } ) )
11 elunitcn 
 |-  ( ( t ` 0 ) e. ( 0 [,] 1 ) -> ( t ` 0 ) e. CC )
12 11 adantr 
 |-  ( ( ( t ` 0 ) e. ( 0 [,] 1 ) /\ t = { <. 0 , ( t ` 0 ) >. } ) -> ( t ` 0 ) e. CC )
13 7 10 12 3syl 
 |-  ( t e. ( ( 0 [,] 1 ) ^m { 0 } ) -> ( t ` 0 ) e. CC )
14 fveq2 
 |-  ( k = 0 -> ( t ` k ) = ( t ` 0 ) )
15 14 sumsn 
 |-  ( ( 0 e. ZZ /\ ( t ` 0 ) e. CC ) -> sum_ k e. { 0 } ( t ` k ) = ( t ` 0 ) )
16 6 13 15 sylancr 
 |-  ( t e. ( ( 0 [,] 1 ) ^m { 0 } ) -> sum_ k e. { 0 } ( t ` k ) = ( t ` 0 ) )
17 5 16 eqtrid 
 |-  ( t e. ( ( 0 [,] 1 ) ^m { 0 } ) -> sum_ k e. ( 0 ... 0 ) ( t ` k ) = ( t ` 0 ) )
18 17 eqeq1d 
 |-  ( t e. ( ( 0 [,] 1 ) ^m { 0 } ) -> ( sum_ k e. ( 0 ... 0 ) ( t ` k ) = 1 <-> ( t ` 0 ) = 1 ) )
19 18 rabbiia 
 |-  { t e. ( ( 0 [,] 1 ) ^m { 0 } ) | sum_ k e. ( 0 ... 0 ) ( t ` k ) = 1 } = { t e. ( ( 0 [,] 1 ) ^m { 0 } ) | ( t ` 0 ) = 1 }
20 rabeqsn 
 |-  ( { t e. ( ( 0 [,] 1 ) ^m { 0 } ) | ( t ` 0 ) = 1 } = { { <. 0 , 1 >. } } <-> A. t ( ( t e. ( ( 0 [,] 1 ) ^m { 0 } ) /\ ( t ` 0 ) = 1 ) <-> t = { <. 0 , 1 >. } ) )
21 ovex 
 |-  ( 0 [,] 1 ) e. _V
22 1elunit 
 |-  1 e. ( 0 [,] 1 )
23 k0004lem3 
 |-  ( ( 0 e. ZZ /\ ( 0 [,] 1 ) e. _V /\ 1 e. ( 0 [,] 1 ) ) -> ( ( t e. ( ( 0 [,] 1 ) ^m { 0 } ) /\ ( t ` 0 ) = 1 ) <-> t = { <. 0 , 1 >. } ) )
24 6 21 22 23 mp3an 
 |-  ( ( t e. ( ( 0 [,] 1 ) ^m { 0 } ) /\ ( t ` 0 ) = 1 ) <-> t = { <. 0 , 1 >. } )
25 20 24 mpgbir 
 |-  { t e. ( ( 0 [,] 1 ) ^m { 0 } ) | ( t ` 0 ) = 1 } = { { <. 0 , 1 >. } }
26 4 19 25 3eqtri 
 |-  { t e. ( ( 0 [,] 1 ) ^m ( 0 ... 0 ) ) | sum_ k e. ( 0 ... 0 ) ( t ` k ) = 1 } = { { <. 0 , 1 >. } }
27 0nn0 
 |-  0 e. NN0
28 1 k0004val 
 |-  ( 0 e. NN0 -> ( A ` 0 ) = { t e. ( ( 0 [,] 1 ) ^m ( 0 ... 0 ) ) | sum_ k e. ( 0 ... 0 ) ( t ` k ) = 1 } )
29 27 28 ax-mp 
 |-  ( A ` 0 ) = { t e. ( ( 0 [,] 1 ) ^m ( 0 ... 0 ) ) | sum_ k e. ( 0 ... 0 ) ( t ` k ) = 1 }
30 1z 
 |-  1 e. ZZ
31 s1val 
 |-  ( 1 e. ZZ -> <" 1 "> = { <. 0 , 1 >. } )
32 30 31 ax-mp 
 |-  <" 1 "> = { <. 0 , 1 >. }
33 32 sneqi 
 |-  { <" 1 "> } = { { <. 0 , 1 >. } }
34 26 29 33 3eqtr4i 
 |-  ( A ` 0 ) = { <" 1 "> }