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

Metamath Proof Explorer

Theorem smndex1igid

Description: The composition of the modulo function I and a constant function ( GK ) results in ( GK ) itself. (Contributed by AV, 14-Feb-2024)

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

Proof

Step Hyp Ref Expression
1 smndex1ibas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2 smndex1ibas.n ⊢ 𝑁 ∈ ℕ
3 smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4 smndex1ibas.g ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
5 fconstmpt ⊢ ( ℕ0 × { 𝐾 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 )
6 5 eqcomi ⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) = ( ℕ0 × { 𝐾 } )
7 6 a1i ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) = ( ℕ0 × { 𝐾 } ) )
8 7 coeq2d ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ) = ( 𝐼 ∘ ( ℕ0 × { 𝐾 } ) ) )
9 simpl ⊢ ( ( 𝑛 = 𝐾 ∧ 𝑥 ∈ ℕ0 ) → 𝑛 = 𝐾 )
10 9 mpteq2dva ⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
11 nn0ex ⊢ ℕ0 ∈ V
12 11 mptex ⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V
13 10 4 12 fvmpt ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
14 13 coeq2d ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( 𝐺 ‘ 𝐾 ) ) = ( 𝐼 ∘ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ) )
15 oveq1 ⊢ ( 𝑥 = 𝐾 → ( 𝑥 mod 𝑁 ) = ( 𝐾 mod 𝑁 ) )
16 zmodidfzoimp ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐾 mod 𝑁 ) = 𝐾 )
17 15 16 sylan9eqr ⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 = 𝐾 ) → ( 𝑥 mod 𝑁 ) = 𝐾 )
18 elfzonn0 ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ℕ0 )
19 3 17 18 18 fvmptd2 ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ‘ 𝐾 ) = 𝐾 )
20 19 eqcomd ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 = ( 𝐼 ‘ 𝐾 ) )
21 20 sneqd ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → { 𝐾 } = { ( 𝐼 ‘ 𝐾 ) } )
22 21 xpeq2d ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( ℕ0 × { 𝐾 } ) = ( ℕ0 × { ( 𝐼 ‘ 𝐾 ) } ) )
23 13 6 eqtrdi ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( ℕ0 × { 𝐾 } ) )
24 ovex ⊢ ( 𝑥 mod 𝑁 ) ∈ V
25 24 3 fnmpti ⊢ 𝐼 Fn ℕ0
26 fcoconst ⊢ ( ( 𝐼 Fn ℕ0 ∧ 𝐾 ∈ ℕ0 ) → ( 𝐼 ∘ ( ℕ0 × { 𝐾 } ) ) = ( ℕ0 × { ( 𝐼 ‘ 𝐾 ) } ) )
27 25 18 26 sylancr ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( ℕ0 × { 𝐾 } ) ) = ( ℕ0 × { ( 𝐼 ‘ 𝐾 ) } ) )
28 22 23 27 3eqtr4d ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝐼 ∘ ( ℕ0 × { 𝐾 } ) ) )
29 8 14 28 3eqtr4d ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐼 ∘ ( 𝐺 ‘ 𝐾 ) ) = ( 𝐺 ‘ 𝐾 ) )