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

Metamath Proof Explorer

Theorem smndex1gid

Description: The composition of a constant function ( GK ) with another endofunction on NN0 results in ( GK ) itself. (Contributed by AV, 14-Feb-2024) Avoid ax-rep . (Revised by GG, 2-Apr-2026)

Ref Expression
Hypotheses smndex1ibas.m ⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
smndex1ibas.n ⊢ 𝑁 ∈ ℕ
smndex1ibas.i ⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
smndex1ibas.g ⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
Assertion smndex1gid ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 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 id ⊢ ( 𝑛 = 𝐾 → 𝑛 = 𝐾 )
6 5 mpteq2dv ⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
7 fconstmpt ⊢ ( ℕ0 × { 𝐾 } ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 )
8 nn0ex ⊢ ℕ0 ∈ V
9 snex ⊢ { 𝐾 } ∈ V
10 8 9 xpex ⊢ ( ℕ0 × { 𝐾 } ) ∈ V
11 7 10 eqeltrri ⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V
12 6 4 11 fvmpt ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
13 12 adantl ⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
14 13 adantr ⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
15 eqidd ⊢ ( ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → 𝐾 = 𝐾 )
16 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
17 1 16 efmndbasf ⊢ ( 𝐹 ∈ ( Base ‘ 𝑀 ) → 𝐹 : ℕ0 ⟶ ℕ0 )
18 ffvelcdm ⊢ ( ( 𝐹 : ℕ0 ⟶ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
19 18 ex ⊢ ( 𝐹 : ℕ0 ⟶ ℕ0 → ( 𝑦 ∈ ℕ0 → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 ) )
20 17 19 syl ⊢ ( 𝐹 ∈ ( Base ‘ 𝑀 ) → ( 𝑦 ∈ ℕ0 → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 ) )
21 20 adantr ⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ℕ0 → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 ) )
22 21 imp ⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
23 simplr ⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )
24 14 15 22 23 fvmptd ⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) = 𝐾 )
25 24 mpteq2dva ⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
26 1 2 3 4 smndex1gbas ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) )
27 1 16 efmndbasf ⊢ ( ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) → ( 𝐺 ‘ 𝐾 ) : ℕ0 ⟶ ℕ0 )
28 26 27 syl ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) : ℕ0 ⟶ ℕ0 )
29 fcompt ⊢ ( ( ( 𝐺 ‘ 𝐾 ) : ℕ0 ⟶ ℕ0 ∧ 𝐹 : ℕ0 ⟶ ℕ0 ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
30 28 17 29 syl2anr ⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
31 eqidd ⊢ ( 𝑥 = 𝑦 → 𝐾 = 𝐾 )
32 31 cbvmptv ⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 )
33 6 32 eqtrdi ⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
34 fconstmpt ⊢ ( ℕ0 × { 𝐾 } ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 )
35 34 10 eqeltrri ⊢ ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) ∈ V
36 33 4 35 fvmpt ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
37 36 adantl ⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
38 25 30 37 3eqtr4d ⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝐺 ‘ 𝐾 ) )