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) Avoid ax-rep and shorten proof. (Revised by GG, 2-Apr-2026)

Ref Expression
Hypotheses smndex1ibas.m ⊢ M = EndoFMnd ⁡ ℕ 0
smndex1ibas.n ⊢ N ∈ ℕ
smndex1ibas.i ⊢ I = x ∈ ℕ 0 ⟼ x mod N
smndex1ibas.g ⊢ G = n ∈ 0 ..^ N ⟼ x ∈ ℕ 0 ⟼ n
Assertion smndex1gbas ⊢ K ∈ 0 ..^ N → G ⁡ K ∈ Base M

Proof

Step Hyp Ref Expression
1 smndex1ibas.m ⊢ M = EndoFMnd ⁡ ℕ 0
2 smndex1ibas.n ⊢ N ∈ ℕ
3 smndex1ibas.i ⊢ I = x ∈ ℕ 0 ⟼ x mod N
4 smndex1ibas.g ⊢ G = n ∈ 0 ..^ N ⟼ x ∈ ℕ 0 ⟼ n
5 elfzonn0 ⊢ K ∈ 0 ..^ N → K ∈ ℕ 0
6 5 adantr ⊢ K ∈ 0 ..^ N ∧ x ∈ ℕ 0 → K ∈ ℕ 0
7 6 fmpttd ⊢ K ∈ 0 ..^ N → x ∈ ℕ 0 ⟼ K : ℕ 0 ⟶ ℕ 0
8 nn0ex ⊢ ℕ 0 ∈ V
9 8 8 elmap ⊢ x ∈ ℕ 0 ⟼ K ∈ ℕ 0 ℕ 0 ↔ x ∈ ℕ 0 ⟼ K : ℕ 0 ⟶ ℕ 0
10 7 9 sylibr ⊢ K ∈ 0 ..^ N → x ∈ ℕ 0 ⟼ K ∈ ℕ 0 ℕ 0
11 id ⊢ n = K → n = K
12 11 mpteq2dv ⊢ n = K → x ∈ ℕ 0 ⟼ n = x ∈ ℕ 0 ⟼ K
13 fconstmpt ⊢ ℕ 0 × K = x ∈ ℕ 0 ⟼ K
14 snex ⊢ K ∈ V
15 8 14 xpex ⊢ ℕ 0 × K ∈ V
16 13 15 eqeltrri ⊢ x ∈ ℕ 0 ⟼ K ∈ V
17 12 4 16 fvmpt ⊢ K ∈ 0 ..^ N → G ⁡ K = x ∈ ℕ 0 ⟼ K
18 eqid ⊢ Base M = Base M
19 1 18 efmndbas ⊢ Base M = ℕ 0 ℕ 0
20 19 a1i ⊢ K ∈ 0 ..^ N → Base M = ℕ 0 ℕ 0
21 10 17 20 3eltr4d ⊢ K ∈ 0 ..^ N → G ⁡ K ∈ Base M