Theorem smndex1gbas

Description: The constant functions ( GK ) are endofunctions on NN0 . (Contributed by AV, 12-Feb-2024)

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

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2		smndex1ibas.n	⊢ 𝑁 ∈ ℕ
3		smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4		smndex1ibas.g	⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
5		elfzonn0	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ℕ0 )
6	5	adantr	⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑥 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
7	6	ralrimiva	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ∀ 𝑥 ∈ ℕ0 𝐾 ∈ ℕ0 )
8		eqid	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 )
9	8	fmpt	⊢ ( ∀ 𝑥 ∈ ℕ0 𝐾 ∈ ℕ0 ↔ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) : ℕ0 ⟶ ℕ0 )
10	7 9	sylib	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) : ℕ0 ⟶ ℕ0 )
11		nn0ex	⊢ ℕ0 ∈ V
12	11 11	elmap	⊢ ( ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ ( ℕ0 ↑m ℕ0 ) ↔ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) : ℕ0 ⟶ ℕ0 )
13	10 12	sylibr	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ ( ℕ0 ↑m ℕ0 ) )
14	4	a1i	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) ) )
15		id	⊢ ( 𝑛 = 𝐾 → 𝑛 = 𝐾 )
16	15	mpteq2dv	⊢ ( 𝑛 = 𝐾 → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
17	16	adantl	⊢ ( ( 𝐾 ∈ ( 0 ..^ 𝑁 ) ∧ 𝑛 = 𝐾 ) → ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
18		id	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → 𝐾 ∈ ( 0 ..^ 𝑁 ) )
19	11	mptex	⊢ ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V
20	19	a1i	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) ∈ V )
21	14 17 18 20	fvmptd	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) = ( 𝑥 ∈ ℕ0 ↦ 𝐾 ) )
22		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
23	1 22	efmndbas	⊢ ( Base ‘ 𝑀 ) = ( ℕ0 ↑m ℕ0 )
24	23	a1i	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( Base ‘ 𝑀 ) = ( ℕ0 ↑m ℕ0 ) )
25	13 21 24	3eltr4d	⊢ ( 𝐾 ∈ ( 0 ..^ 𝑁 ) → ( 𝐺 ‘ 𝐾 ) ∈ ( Base ‘ 𝑀 ) )