Theorem smndex1id

Description: The modulo function I is the identity of the monoid of endofunctions on NN0 restricted to the modulo function I and the constant functions ( GK ) . (Contributed by AV, 16-Feb-2024)

	Ref	Expression
Hypotheses	smndex1ibas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
	smndex1ibas.n	⊢ 𝑁 ∈ ℕ
	smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
	smndex1ibas.g	⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
	smndex1mgm.b	⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
	smndex1mgm.s	⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
Assertion	smndex1id	⊢ 𝐼 = ( 0g ‘ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	⊢ 𝑀 = ( EndoFMnd ‘ ℕ0 )
2		smndex1ibas.n	⊢ 𝑁 ∈ ℕ
3		smndex1ibas.i	⊢ 𝐼 = ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) )
4		smndex1ibas.g	⊢ 𝐺 = ( 𝑛 ∈ ( 0 ..^ 𝑁 ) ↦ ( 𝑥 ∈ ℕ0 ↦ 𝑛 ) )
5		smndex1mgm.b	⊢ 𝐵 = ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
6		smndex1mgm.s	⊢ 𝑆 = ( 𝑀 ↾s 𝐵 )
7		nn0ex	⊢ ℕ0 ∈ V
8	7	mptex	⊢ ( 𝑥 ∈ ℕ0 ↦ ( 𝑥 mod 𝑁 ) ) ∈ V
9	3 8	eqeltri	⊢ 𝐼 ∈ V
10	9	snid	⊢ 𝐼 ∈ { 𝐼 }
11		elun1	⊢ ( 𝐼 ∈ { 𝐼 } → 𝐼 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) )
12	10 11	ax-mp	⊢ 𝐼 ∈ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } )
13	12 5	eleqtrri	⊢ 𝐼 ∈ 𝐵
14	1 2 3 4 5 6	smndex1bas	⊢ ( Base ‘ 𝑆 ) = 𝐵
15	14	eqcomi	⊢ 𝐵 = ( Base ‘ 𝑆 )
16	15	a1i	⊢ ( 𝐼 ∈ 𝐵 → 𝐵 = ( Base ‘ 𝑆 ) )
17		snex	⊢ { 𝐼 } ∈ V
18		ovex	⊢ ( 0 ..^ 𝑁 ) ∈ V
19		snex	⊢ { ( 𝐺 ‘ 𝑛 ) } ∈ V
20	18 19	iunex	⊢ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ∈ V
21	17 20	unex	⊢ ( { 𝐼 } ∪ ∪ 𝑛 ∈ ( 0 ..^ 𝑁 ) { ( 𝐺 ‘ 𝑛 ) } ) ∈ V
22	5 21	eqeltri	⊢ 𝐵 ∈ V
23		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
24	6 23	ressplusg	⊢ ( 𝐵 ∈ V → ( +g ‘ 𝑀 ) = ( +g ‘ 𝑆 ) )
25	22 24	mp1i	⊢ ( 𝐼 ∈ 𝐵 → ( +g ‘ 𝑀 ) = ( +g ‘ 𝑆 ) )
26		id	⊢ ( 𝐼 ∈ 𝐵 → 𝐼 ∈ 𝐵 )
27	1 2 3	smndex1ibas	⊢ 𝐼 ∈ ( Base ‘ 𝑀 )
28	27	a1i	⊢ ( 𝐼 ∈ 𝐵 → 𝐼 ∈ ( Base ‘ 𝑀 ) )
29	1 2 3 4 5	smndex1basss	⊢ 𝐵 ⊆ ( Base ‘ 𝑀 )
30	29	sseli	⊢ ( 𝑎 ∈ 𝐵 → 𝑎 ∈ ( Base ‘ 𝑀 ) )
31		eqid	⊢ ( Base ‘ 𝑀 ) = ( Base ‘ 𝑀 )
32	1 31 23	efmndov	⊢ ( ( 𝐼 ∈ ( Base ‘ 𝑀 ) ∧ 𝑎 ∈ ( Base ‘ 𝑀 ) ) → ( 𝐼 ( +g ‘ 𝑀 ) 𝑎 ) = ( 𝐼 ∘ 𝑎 ) )
33	28 30 32	syl2an	⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐼 ( +g ‘ 𝑀 ) 𝑎 ) = ( 𝐼 ∘ 𝑎 ) )
34	1 2 3 4 5 6	smndex1mndlem	⊢ ( 𝑎 ∈ 𝐵 → ( ( 𝐼 ∘ 𝑎 ) = 𝑎 ∧ ( 𝑎 ∘ 𝐼 ) = 𝑎 ) )
35	34	simpld	⊢ ( 𝑎 ∈ 𝐵 → ( 𝐼 ∘ 𝑎 ) = 𝑎 )
36	35	adantl	⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐼 ∘ 𝑎 ) = 𝑎 )
37	33 36	eqtrd	⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝐼 ( +g ‘ 𝑀 ) 𝑎 ) = 𝑎 )
38	1 31 23	efmndov	⊢ ( ( 𝑎 ∈ ( Base ‘ 𝑀 ) ∧ 𝐼 ∈ ( Base ‘ 𝑀 ) ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝐼 ) = ( 𝑎 ∘ 𝐼 ) )
39	30 28 38	syl2anr	⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝐼 ) = ( 𝑎 ∘ 𝐼 ) )
40	34	simprd	⊢ ( 𝑎 ∈ 𝐵 → ( 𝑎 ∘ 𝐼 ) = 𝑎 )
41	40	adantl	⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 ∘ 𝐼 ) = 𝑎 )
42	39 41	eqtrd	⊢ ( ( 𝐼 ∈ 𝐵 ∧ 𝑎 ∈ 𝐵 ) → ( 𝑎 ( +g ‘ 𝑀 ) 𝐼 ) = 𝑎 )
43	16 25 26 37 42	grpidd	⊢ ( 𝐼 ∈ 𝐵 → 𝐼 = ( 0g ‘ 𝑆 ) )
44	13 43	ax-mp	⊢ 𝐼 = ( 0g ‘ 𝑆 )