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)

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 4 a1i ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) ) )
6 id ⊢ ( 𝑛 = 𝐾 → 𝑛 = 𝐾 )
7 6 mpteq2dv ⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
8 7 adantl ⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑛 = 𝐾 ) → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
9 id ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )
10 nn0ex ⊢ ℕ0 ∈ V
11 10 mptex ⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V
12 11 a1i ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V )
13 5 8 9 12 fvmptd ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
14 13 adantl ⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
15 14 adantr ⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
16 eqidd ⊢ ( ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) ∧ 𝑥 = ( 𝐹 ‘ 𝑦 ) ) → 𝐾 = 𝐾 )
17 eqid ⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
18 1 17 efmndbasf ⊢ ( 𝐹 ∈ ( Base ‘ 𝑀 ) → 𝐹 : ℕ0 ⟶ ℕ0 )
19 ffvelcdm ⊢ ( ( 𝐹 : ℕ0 ⟶ ℕ0 ∧ 𝑦 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
20 19 ex ⊢ ( 𝐹 : ℕ0 ⟶ ℕ0 → ( 𝑦 ∈ ℕ0 → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 ) )
21 18 20 syl ⊢ ( 𝐹 ∈ ( Base ‘ 𝑀 ) → ( 𝑦 ∈ ℕ0 → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 ) )
22 21 adantr ⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ℕ0 → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 ) )
23 22 imp ⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℕ0 )
24 simplr ⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )
25 15 16 23 24 fvmptd ⊢ ( ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) ∧ 𝑦 ∈ ℕ0 ) → ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) = 𝐾 )
26 25 mpteq2dva ⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
27 1 2 3 4 smndex1gbas ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) )
28 1 17 efmndbasf ⊢ ( ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) → ( 𝐺 ‘ 𝐾 ) : ℕ0 ⟶ ℕ0 )
29 27 28 syl ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) : ℕ0 ⟶ ℕ0 )
30 fcompt ⊢ ( ( ( 𝐺 ‘ 𝐾 ) : ℕ0 ⟶ ℕ0 ∧ 𝐹 : ℕ0 ⟶ ℕ0 ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
31 29 18 30 syl2anr ⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝑦 ∈ ℕ0 ↦ ( ( 𝐺 ‘ 𝐾 ) ‘ ( 𝐹 ‘ 𝑦 ) ) ) )
32 eqidd ⊢ ( 𝑥 = 𝑦 → 𝐾 = 𝐾 )
33 32 cbvmptv ⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 )
34 7 33 eqtrdi ⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
35 34 adantl ⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑛 = 𝐾 ) → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
36 10 mptex ⊢ ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) ∈ V
37 36 a1i ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) ∈ V )
38 5 35 9 37 fvmptd ⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
39 38 adantl ⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑦 ∈ ℕ0 ↦ 𝐾 ) )
40 26 31 39 3eqtr4d ⊢ ( ( 𝐹 ∈ ( Base ‘ 𝑀 ) ∧ 𝐾 ∈ ( 0 ..^ 𝑁 ) ) → ( ( 𝐺 ‘ 𝐾 ) ∘ 𝐹 ) = ( 𝐺 ‘ 𝐾 ) )