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∈ℕ0⟼t∈011…n+1|∑k=1n+1t⁡k=1
Assertion k0004val0 ⊢A⁡0=11

Proof

Step Hyp Ref Expression
1 k0004.a ⊢A=n∈ℕ0⟼t∈011…n+1|∑k=1n+1t⁡k=1
2 0nn0 ⊢0∈ℕ0
3 1 k0004val ⊢0∈ℕ0→A⁡0=t∈011…0+1|∑k=10+1t⁡k=1
4 2 3 ax-mp ⊢A⁡0=t∈011…0+1|∑k=10+1t⁡k=1
5 0p1e1 ⊢0+1=1
6 5 oveq2i ⊢1…0+1=1…1
7 1z ⊢1∈ℤ
8 fzsn ⊢1∈ℤ→1…1=1
9 7 8 ax-mp ⊢1…1=1
10 6 9 eqtri ⊢1…0+1=1
11 10 oveq2i ⊢011…0+1=011
12 11 rabeqi ⊢t∈011…0+1|∑k=10+1t⁡k=1=t∈011|∑k=10+1t⁡k=1
13 10 sumeq1i ⊢∑k=10+1t⁡k=∑k∈1t⁡k
14 elmapi ⊢t∈011→t:1⟶01
15 fsn2g ⊢1∈ℤ→t:1⟶01↔t⁡1∈01∧t=1t⁡1
16 7 15 ax-mp ⊢t:1⟶01↔t⁡1∈01∧t=1t⁡1
17 16 biimpi ⊢t:1⟶01→t⁡1∈01∧t=1t⁡1
18 unitssre ⊢01⊆ℝ
19 ax-resscn ⊢ℝ⊆ℂ
20 18 19 sstri ⊢01⊆ℂ
21 20 sseli ⊢t⁡1∈01→t⁡1∈ℂ
22 21 adantr ⊢t⁡1∈01∧t=1t⁡1→t⁡1∈ℂ
23 14 17 22 3syl ⊢t∈011→t⁡1∈ℂ
24 fveq2 ⊢k=1→t⁡k=t⁡1
25 24 sumsn ⊢1∈ℤ∧t⁡1∈ℂ→∑k∈1t⁡k=t⁡1
26 7 23 25 sylancr ⊢t∈011→∑k∈1t⁡k=t⁡1
27 13 26 eqtrid ⊢t∈011→∑k=10+1t⁡k=t⁡1
28 27 eqeq1d ⊢t∈011→∑k=10+1t⁡k=1↔t⁡1=1
29 28 rabbiia ⊢t∈011|∑k=10+1t⁡k=1=t∈011|t⁡1=1
30 12 29 eqtri ⊢t∈011…0+1|∑k=10+1t⁡k=1=t∈011|t⁡1=1
31 rabeqsn ⊢t∈011|t⁡1=1=11↔∀tt∈011∧t⁡1=1↔t=11
32 ovex ⊢01∈V
33 1elunit ⊢1∈01
34 k0004lem3 ⊢1∈ℤ∧01∈V∧1∈01→t∈011∧t⁡1=1↔t=11
35 7 32 33 34 mp3an ⊢t∈011∧t⁡1=1↔t=11
36 31 35 mpgbir ⊢t∈011|t⁡1=1=11
37 30 36 eqtri ⊢t∈011…0+1|∑k=10+1t⁡k=1=11
38 4 37 eqtri ⊢A⁡0=11