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 ( 0 ... 𝑛 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑡 ‘ 𝑘 ) = 1 } )
Assertion	k0004val0	⊢ ( 𝐴 ‘ 0 ) = { ⟨“ 1 ”⟩ }

Proof

Step	Hyp	Ref	Expression
1		k0004.a	⊢ 𝐴 = ( 𝑛 ∈ ℕ0 ↦ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 𝑛 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑡 ‘ 𝑘 ) = 1 } )
2		fz0sn	⊢ ( 0 ... 0 ) = { 0 }
3	2	oveq2i	⊢ ( ( 0 [,] 1 ) ↑m ( 0 ... 0 ) ) = ( ( 0 [,] 1 ) ↑m { 0 } )
4	3	rabeqi	⊢ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 0 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑡 ‘ 𝑘 ) = 1 } = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) ∣ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑡 ‘ 𝑘 ) = 1 }
5	2	sumeq1i	⊢ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑡 ‘ 𝑘 ) = Σ 𝑘 ∈ { 0 } ( 𝑡 ‘ 𝑘 )
6		0z	⊢ 0 ∈ ℤ
7		elmapi	⊢ ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) → 𝑡 : { 0 } ⟶ ( 0 [,] 1 ) )
8		fsn2g	⊢ ( 0 ∈ ℤ → ( 𝑡 : { 0 } ⟶ ( 0 [,] 1 ) ↔ ( ( 𝑡 ‘ 0 ) ∈ ( 0 [,] 1 ) ∧ 𝑡 = { ⟨ 0 , ( 𝑡 ‘ 0 ) ⟩ } ) ) )
9	6 8	ax-mp	⊢ ( 𝑡 : { 0 } ⟶ ( 0 [,] 1 ) ↔ ( ( 𝑡 ‘ 0 ) ∈ ( 0 [,] 1 ) ∧ 𝑡 = { ⟨ 0 , ( 𝑡 ‘ 0 ) ⟩ } ) )
10	9	biimpi	⊢ ( 𝑡 : { 0 } ⟶ ( 0 [,] 1 ) → ( ( 𝑡 ‘ 0 ) ∈ ( 0 [,] 1 ) ∧ 𝑡 = { ⟨ 0 , ( 𝑡 ‘ 0 ) ⟩ } ) )
11		elunitcn	⊢ ( ( 𝑡 ‘ 0 ) ∈ ( 0 [,] 1 ) → ( 𝑡 ‘ 0 ) ∈ ℂ )
12	11	adantr	⊢ ( ( ( 𝑡 ‘ 0 ) ∈ ( 0 [,] 1 ) ∧ 𝑡 = { ⟨ 0 , ( 𝑡 ‘ 0 ) ⟩ } ) → ( 𝑡 ‘ 0 ) ∈ ℂ )
13	7 10 12	3syl	⊢ ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) → ( 𝑡 ‘ 0 ) ∈ ℂ )
14		fveq2	⊢ ( 𝑘 = 0 → ( 𝑡 ‘ 𝑘 ) = ( 𝑡 ‘ 0 ) )
15	14	sumsn	⊢ ( ( 0 ∈ ℤ ∧ ( 𝑡 ‘ 0 ) ∈ ℂ ) → Σ 𝑘 ∈ { 0 } ( 𝑡 ‘ 𝑘 ) = ( 𝑡 ‘ 0 ) )
16	6 13 15	sylancr	⊢ ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) → Σ 𝑘 ∈ { 0 } ( 𝑡 ‘ 𝑘 ) = ( 𝑡 ‘ 0 ) )
17	5 16	eqtrid	⊢ ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑡 ‘ 𝑘 ) = ( 𝑡 ‘ 0 ) )
18	17	eqeq1d	⊢ ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) → ( Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑡 ‘ 𝑘 ) = 1 ↔ ( 𝑡 ‘ 0 ) = 1 ) )
19	18	rabbiia	⊢ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) ∣ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑡 ‘ 𝑘 ) = 1 } = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) ∣ ( 𝑡 ‘ 0 ) = 1 }
20		rabeqsn	⊢ ( { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) ∣ ( 𝑡 ‘ 0 ) = 1 } = { { ⟨ 0 , 1 ⟩ } } ↔ ∀ 𝑡 ( ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) ∧ ( 𝑡 ‘ 0 ) = 1 ) ↔ 𝑡 = { ⟨ 0 , 1 ⟩ } ) )
21		ovex	⊢ ( 0 [,] 1 ) ∈ V
22		1elunit	⊢ 1 ∈ ( 0 [,] 1 )
23		k0004lem3	⊢ ( ( 0 ∈ ℤ ∧ ( 0 [,] 1 ) ∈ V ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) ∧ ( 𝑡 ‘ 0 ) = 1 ) ↔ 𝑡 = { ⟨ 0 , 1 ⟩ } ) )
24	6 21 22 23	mp3an	⊢ ( ( 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) ∧ ( 𝑡 ‘ 0 ) = 1 ) ↔ 𝑡 = { ⟨ 0 , 1 ⟩ } )
25	20 24	mpgbir	⊢ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m { 0 } ) ∣ ( 𝑡 ‘ 0 ) = 1 } = { { ⟨ 0 , 1 ⟩ } }
26	4 19 25	3eqtri	⊢ { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 0 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑡 ‘ 𝑘 ) = 1 } = { { ⟨ 0 , 1 ⟩ } }
27		0nn0	⊢ 0 ∈ ℕ0
28	1	k0004val	⊢ ( 0 ∈ ℕ0 → ( 𝐴 ‘ 0 ) = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 0 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑡 ‘ 𝑘 ) = 1 } )
29	27 28	ax-mp	⊢ ( 𝐴 ‘ 0 ) = { 𝑡 ∈ ( ( 0 [,] 1 ) ↑m ( 0 ... 0 ) ) ∣ Σ 𝑘 ∈ ( 0 ... 0 ) ( 𝑡 ‘ 𝑘 ) = 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	⊢ ( 𝐴 ‘ 0 ) = { ⟨“ 1 ”⟩ }