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

Proof

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