Theorem smndex1gbas

Description: The constant functions ( GK ) are endofunctions on NN0 . (Contributed by AV, 12-Feb-2024) Avoid ax-rep and shorten proof. (Revised by GG, 2-Apr-2026)

	Ref	Expression
Hypotheses	smndex1ibas.m	|- M = ( EndoFMnd ` NN0 )
	smndex1ibas.n	|- N e. NN
	smndex1ibas.i	|- I = ( x e. NN0 |-> ( x mod N ) )
	smndex1ibas.g	|- G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) )
Assertion	smndex1gbas	|- ( K e. ( 0 ..^ N ) -> ( G ` K ) e. ( Base ` M ) )

Proof

Step	Hyp	Ref	Expression
1		smndex1ibas.m	|- M = ( EndoFMnd ` NN0 )
2		smndex1ibas.n	|- N e. NN
3		smndex1ibas.i	|- I = ( x e. NN0 |-> ( x mod N ) )
4		smndex1ibas.g	|- G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) )
5		elfzonn0	|- ( K e. ( 0 ..^ N ) -> K e. NN0 )
6	5	adantr	|- ( ( K e. ( 0 ..^ N ) /\ x e. NN0 ) -> K e. NN0 )
7	6	fmpttd	|- ( K e. ( 0 ..^ N ) -> ( x e. NN0 |-> K ) : NN0 --> NN0 )
8		nn0ex	|- NN0 e. _V
9	8 8	elmap	|- ( ( x e. NN0 |-> K ) e. ( NN0 ^m NN0 ) <-> ( x e. NN0 |-> K ) : NN0 --> NN0 )
10	7 9	sylibr	|- ( K e. ( 0 ..^ N ) -> ( x e. NN0 |-> K ) e. ( NN0 ^m NN0 ) )
11		id	|- ( n = K -> n = K )
12	11	mpteq2dv	|- ( n = K -> ( x e. NN0 |-> n ) = ( x e. NN0 |-> K ) )
13		fconstmpt	|- ( NN0 X. { K } ) = ( x e. NN0 |-> K )
14		snex	|- { K } e. _V
15	8 14	xpex	|- ( NN0 X. { K } ) e. _V
16	13 15	eqeltrri	|- ( x e. NN0 |-> K ) e. _V
17	12 4 16	fvmpt	|- ( K e. ( 0 ..^ N ) -> ( G ` K ) = ( x e. NN0 |-> K ) )
18		eqid	|- ( Base ` M ) = ( Base ` M )
19	1 18	efmndbas	|- ( Base ` M ) = ( NN0 ^m NN0 )
20	19	a1i	|- ( K e. ( 0 ..^ N ) -> ( Base ` M ) = ( NN0 ^m NN0 ) )
21	10 17 20	3eltr4d	|- ( K e. ( 0 ..^ N ) -> ( G ` K ) e. ( Base ` M ) )