This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem smndex1gbas

Description: The constant functions ( GK ) are endofunctions on NN0 . (Contributed by AV, 12-Feb-2024)

Ref Expression
Hypotheses smndex1ibas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
smndex1ibas.n ⊢ 𝑁 ∈ ℕ
smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
smndex1ibas.g ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
Assertion smndex1gbas ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 smndex1ibas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2 smndex1ibas.n ⊢ 𝑁 ∈ ℕ
3 smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4 smndex1ibas.g ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
5 elfzonn0 ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ℕ0 )
6 5 adantr ⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
7 6 ralrimiva ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ∀ 𝑥 ∈ ℕ0 𝐾 ∈ ℕ0 )
8 eqid ⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 )
9 8 fmpt ⊢ ( ∀ 𝑥 ∈ ℕ0 𝐾 ∈ ℕ0 ↔ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) : ℕ0 ⟶ ℕ0 )
10 7 9 sylib ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) : ℕ0 ⟶ ℕ0 )
11 nn0ex ⊢ ℕ0 ∈ V
12 11 11 elmap ⊢ ( ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ ( ℕ0 ↑m ℕ0 ) ↔ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) : ℕ0 ⟶ ℕ0 )
13 10 12 sylibr ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ ( ℕ0 ↑m ℕ0 ) )
14 4 a1i ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) ) )
15 id ⊢ ( 𝑛 = 𝐾 → 𝑛 = 𝐾 )
16 15 mpteq2dv ⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
17 16 adantl ⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑛 = 𝐾 ) → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
18 id ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )
19 11 mptex ⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V
20 19 a1i ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V )
21 14 17 18 20 fvmptd ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
22 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
23 1 22 efmndbas ⊢ ( Base ‘ 𝑀 ) = ( ℕ0 ↑m ℕ0 )
24 23 a1i ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( Base ‘ 𝑀 ) = ( ℕ0 ↑m ℕ0 ) )
25 13 21 24 3eltr4d ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) )