Theorem k0004val0

Description: The topological simplex of dimension 0 is a singleton. (Contributed by RP, 2-Apr-2021)

	Ref	Expression
Hypothesis	k0004.a	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑛 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } )
Assertion	k0004val0	⊢ ( 𝐴 ‘ 0 ) = { { ⟨ 1 , 1 ⟩ } }

Proof

Step	Hyp	Ref	Expression
1		k0004.a	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 𝑛 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 𝑛 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } )
2		0nn0	⊢ 0 ∈ ℕ0
3	1	k0004val	⊢ ( 0 ∈ ℕ0 → ( 𝐴 ‘ 0 ) = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 0 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 0 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } )
4	2 3	ax-mp	⊢ ( 𝐴 ‘ 0 ) = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 0 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 0 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 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 ) ↑m ( 1 ... ( 0 + 1 ) ) ) = ( ( 0 [,] 1 ) ↑m { 1 } )
12	11	rabeqi	⊢ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 0 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 0 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) ∣ Σ 𝑘 ∈ ( 1 ... ( 0 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 }
13	10	sumeq1i	⊢ Σ 𝑘 ∈ ( 1 ... ( 0 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = Σ 𝑘 ∈ { 1 } ( 𝑡 ‘ 𝑘 )
14		elmapi	⊢ ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) → 𝑡 : { 1 } ⟶ ( 0 [,] 1 ) )
15		fsn2g	⊢ ( 1 ∈ ℤ → ( 𝑡 : { 1 } ⟶ ( 0 [,] 1 ) ↔ ( ( 𝑡 ‘ 1 ) ∈ ( 0 [,] 1 ) ∧ 𝑡 = { ⟨ 1 , ( 𝑡 ‘ 1 ) ⟩ } ) ) )
16	7 15	ax-mp	⊢ ( 𝑡 : { 1 } ⟶ ( 0 [,] 1 ) ↔ ( ( 𝑡 ‘ 1 ) ∈ ( 0 [,] 1 ) ∧ 𝑡 = { ⟨ 1 , ( 𝑡 ‘ 1 ) ⟩ } ) )
17	16	biimpi	⊢ ( 𝑡 : { 1 } ⟶ ( 0 [,] 1 ) → ( ( 𝑡 ‘ 1 ) ∈ ( 0 [,] 1 ) ∧ 𝑡 = { ⟨ 1 , ( 𝑡 ‘ 1 ) ⟩ } ) )
18		unitssre	⊢ ( 0 [,] 1 ) ⊆ ℝ
19		ax-resscn	⊢ ℝ ⊆ ℂ
20	18 19	sstri	⊢ ( 0 [,] 1 ) ⊆ ℂ
21	20	sseli	⊢ ( ( 𝑡 ‘ 1 ) ∈ ( 0 [,] 1 ) → ( 𝑡 ‘ 1 ) ∈ ℂ )
22	21	adantr	⊢ ( ( ( 𝑡 ‘ 1 ) ∈ ( 0 [,] 1 ) ∧ 𝑡 = { ⟨ 1 , ( 𝑡 ‘ 1 ) ⟩ } ) → ( 𝑡 ‘ 1 ) ∈ ℂ )
23	14 17 22	3syl	⊢ ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) → ( 𝑡 ‘ 1 ) ∈ ℂ )
24		fveq2	⊢ ( 𝑘 = 1 → ( 𝑡 ‘ 𝑘 ) = ( 𝑡 ‘ 1 ) )
25	24	sumsn	⊢ ( ( 1 ∈ ℤ ∧ ( 𝑡 ‘ 1 ) ∈ ℂ ) → Σ 𝑘 ∈ { 1 } ( 𝑡 ‘ 𝑘 ) = ( 𝑡 ‘ 1 ) )
26	7 23 25	sylancr	⊢ ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) → Σ 𝑘 ∈ { 1 } ( 𝑡 ‘ 𝑘 ) = ( 𝑡 ‘ 1 ) )
27	13 26	syl5eq	⊢ ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) → Σ 𝑘 ∈ ( 1 ... ( 0 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = ( 𝑡 ‘ 1 ) )
28	27	eqeq1d	⊢ ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) → ( Σ 𝑘 ∈ ( 1 ... ( 0 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 ↔ ( 𝑡 ‘ 1 ) = 1 ) )
29	28	rabbiia	⊢ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) ∣ Σ 𝑘 ∈ ( 1 ... ( 0 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) ∣ ( 𝑡 ‘ 1 ) = 1 }
30	12 29	eqtri	⊢ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 0 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 0 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) ∣ ( 𝑡 ‘ 1 ) = 1 }
31		rabeqsn	⊢ ( { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) ∣ ( 𝑡 ‘ 1 ) = 1 } = { { ⟨ 1 , 1 ⟩ } } ↔ ∀ 𝑡 ( ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) ∧ ( 𝑡 ‘ 1 ) = 1 ) ↔ 𝑡 = { ⟨ 1 , 1 ⟩ } ) )
32		ovex	⊢ ( 0 [,] 1 ) ∈ V
33		1elunit	⊢ 1 ∈ ( 0 [,] 1 )
34		k0004lem3	⊢ ( ( 1 ∈ ℤ ∧ ( 0 [,] 1 ) ∈ V ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) ∧ ( 𝑡 ‘ 1 ) = 1 ) ↔ 𝑡 = { ⟨ 1 , 1 ⟩ } ) )
35	7 32 33 34	mp3an	⊢ ( ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) ∧ ( 𝑡 ‘ 1 ) = 1 ) ↔ 𝑡 = { ⟨ 1 , 1 ⟩ } )
36	31 35	mpgbir	⊢ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 1 } ) ∣ ( 𝑡 ‘ 1 ) = 1 } = { { ⟨ 1 , 1 ⟩ } }
37	30 36	eqtri	⊢ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 1 ... ( 0 + 1 ) ) ) ∣ Σ 𝑘 ∈ ( 1 ... ( 0 + 1 ) ) ( 𝑡 ‘ 𝑘 ) = 1 } = { { ⟨ 1 , 1 ⟩ } }
38	4 37	eqtri	⊢ ( 𝐴 ‘ 0 ) = { { ⟨ 1 , 1 ⟩ } }