Metamath Proof Explorer


Theorem smndex1ibas

Description: The modulo function I is an endofunction on NN0 . (Contributed by AV, 12-Feb-2024)

Ref Expression
Hypotheses smndex1ibas.m 𝑀 = ( EndoFMnd ‘ ℕ0 )
smndex1ibas.n 𝑁 ∈ ℕ
smndex1ibas.i 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
Assertion smndex1ibas 𝐼 ∈ ( Base ‘ 𝑀 )

Proof

Step Hyp Ref Expression
1 smndex1ibas.m 𝑀 = ( EndoFMnd ‘ ℕ0 )
2 smndex1ibas.n 𝑁 ∈ ℕ
3 smndex1ibas.i 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4 eqid ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
5 nn0z ( 𝑥 ∈ ℕ0𝑥 ∈ ℤ )
6 2 a1i ( 𝑥 ∈ ℕ0𝑁 ∈ ℕ )
7 5 6 zmodcld ( 𝑥 ∈ ℕ0 → ( 𝑥 mod 𝑁 ) ∈ ℕ0 )
8 4 7 fmpti ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) : ℕ0 ⟶ ℕ0
9 nn0ex 0 ∈ V
10 9 9 elmap ( ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) ∈ ( ℕ0m0 ) ↔ ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) : ℕ0 ⟶ ℕ0 )
11 8 10 mpbir ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) ∈ ( ℕ0m0 )
12 eqid ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
13 1 12 efmndbas ( Base ‘ 𝑀 ) = ( ℕ0m0 )
14 11 3 13 3eltr4i 𝐼 ∈ ( Base ‘ 𝑀 )