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 0 … n | ∑ k = 0 n t ⁡ k = 1
Assertion k0004val0 ⊢ A ⁡ 0 = ⟨“ 1 ”⟩

Proof

Step Hyp Ref Expression
1 k0004.a ⊢ A = n ∈ ℕ 0 ⟼ t ∈ 0 1 0 … n | ∑ k = 0 n t ⁡ k = 1
2 fz0sn ⊢ 0 … 0 = 0
3 2 oveq2i ⊢ 0 1 0 … 0 = 0 1 0
4 3 rabeqi ⊢ t ∈ 0 1 0 … 0 | ∑ k = 0 0 t ⁡ k = 1 = t ∈ 0 1 0 | ∑ k = 0 0 t ⁡ k = 1
5 2 sumeq1i ⊢ ∑ k = 0 0 t ⁡ k = ∑ k ∈ 0 t ⁡ k
6 0z ⊢ 0 ∈ ℤ
7 elmapi ⊢ t ∈ 0 1 0 → t : 0 ⟶ 0 1
8 fsn2g ⊢ 0 ∈ ℤ → t : 0 ⟶ 0 1 ↔ t ⁡ 0 ∈ 0 1 ∧ t = 0 t ⁡ 0
9 6 8 ax-mp ⊢ t : 0 ⟶ 0 1 ↔ t ⁡ 0 ∈ 0 1 ∧ t = 0 t ⁡ 0
10 9 biimpi ⊢ t : 0 ⟶ 0 1 → t ⁡ 0 ∈ 0 1 ∧ t = 0 t ⁡ 0
11 elunitcn ⊢ t ⁡ 0 ∈ 0 1 → t ⁡ 0 ∈ ℂ
12 11 adantr ⊢ t ⁡ 0 ∈ 0 1 ∧ t = 0 t ⁡ 0 → t ⁡ 0 ∈ ℂ
13 7 10 12 3syl ⊢ t ∈ 0 1 0 → t ⁡ 0 ∈ ℂ
14 fveq2 ⊢ k = 0 → t ⁡ k = t ⁡ 0
15 14 sumsn ⊢ 0 ∈ ℤ ∧ t ⁡ 0 ∈ ℂ → ∑ k ∈ 0 t ⁡ k = t ⁡ 0
16 6 13 15 sylancr ⊢ t ∈ 0 1 0 → ∑ k ∈ 0 t ⁡ k = t ⁡ 0
17 5 16 eqtrid ⊢ t ∈ 0 1 0 → ∑ k = 0 0 t ⁡ k = t ⁡ 0
18 17 eqeq1d ⊢ t ∈ 0 1 0 → ∑ k = 0 0 t ⁡ k = 1 ↔ t ⁡ 0 = 1
19 18 rabbiia ⊢ t ∈ 0 1 0 | ∑ k = 0 0 t ⁡ k = 1 = t ∈ 0 1 0 | t ⁡ 0 = 1
20 rabeqsn ⊢ t ∈ 0 1 0 | t ⁡ 0 = 1 = 0 1 ↔ ∀ t t ∈ 0 1 0 ∧ t ⁡ 0 = 1 ↔ t = 0 1
21 ovex ⊢ 0 1 ∈ V
22 1elunit ⊢ 1 ∈ 0 1
23 k0004lem3 ⊢ 0 ∈ ℤ ∧ 0 1 ∈ V ∧ 1 ∈ 0 1 → t ∈ 0 1 0 ∧ t ⁡ 0 = 1 ↔ t = 0 1
24 6 21 22 23 mp3an ⊢ t ∈ 0 1 0 ∧ t ⁡ 0 = 1 ↔ t = 0 1
25 20 24 mpgbir ⊢ t ∈ 0 1 0 | t ⁡ 0 = 1 = 0 1
26 4 19 25 3eqtri ⊢ t ∈ 0 1 0 … 0 | ∑ k = 0 0 t ⁡ k = 1 = 0 1
27 0nn0 ⊢ 0 ∈ ℕ 0
28 1 k0004val ⊢ 0 ∈ ℕ 0 → A ⁡ 0 = t ∈ 0 1 0 … 0 | ∑ k = 0 0 t ⁡ k = 1
29 27 28 ax-mp ⊢ A ⁡ 0 = t ∈ 0 1 0 … 0 | ∑ k = 0 0 t ⁡ k = 1
30 1z ⊢ 1 ∈ ℤ
31 s1val ⊢ 1 ∈ ℤ → ⟨“ 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 ”⟩