Theorem smndex1gbas

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

	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	ralrimiva	|- ( K e. ( 0 ..^ N ) -> A. x e. NN0 K e. NN0 )
8		eqid	|- ( x e. NN0 |-> K ) = ( x e. NN0 |-> K )
9	8	fmpt	|- ( A. x e. NN0 K e. NN0 <-> ( x e. NN0 |-> K ) : NN0 --> NN0 )
10	7 9	sylib	|- ( K e. ( 0 ..^ N ) -> ( x e. NN0 |-> K ) : NN0 --> NN0 )
11		nn0ex	|- NN0 e. _V
12	11 11	elmap	|- ( ( x e. NN0 |-> K ) e. ( NN0 ^m NN0 ) <-> ( x e. NN0 |-> K ) : NN0 --> NN0 )
13	10 12	sylibr	|- ( K e. ( 0 ..^ N ) -> ( x e. NN0 |-> K ) e. ( NN0 ^m NN0 ) )
14	4	a1i	|- ( K e. ( 0 ..^ N ) -> G = ( n e. ( 0 ..^ N ) |-> ( x e. NN0 |-> n ) ) )
15		id	|- ( n = K -> n = K )
16	15	mpteq2dv	|- ( n = K -> ( x e. NN0 |-> n ) = ( x e. NN0 |-> K ) )
17	16	adantl	|- ( ( K e. ( 0 ..^ N ) /\ n = K ) -> ( x e. NN0 |-> n ) = ( x e. NN0 |-> K ) )
18		id	|- ( K e. ( 0 ..^ N ) -> K e. ( 0 ..^ N ) )
19	11	mptex	|- ( x e. NN0 |-> K ) e. _V
20	19	a1i	|- ( K e. ( 0 ..^ N ) -> ( x e. NN0 |-> K ) e. _V )
21	14 17 18 20	fvmptd	|- ( K e. ( 0 ..^ N ) -> ( G ` K ) = ( x e. NN0 |-> K ) )
22		eqid	|- ( Base ` M ) = ( Base ` M )
23	1 22	efmndbas	|- ( Base ` M ) = ( NN0 ^m NN0 )
24	23	a1i	|- ( K e. ( 0 ..^ N ) -> ( Base ` M ) = ( NN0 ^m NN0 ) )
25	13 21 24	3eltr4d	|- ( K e. ( 0 ..^ N ) -> ( G ` K ) e. ( Base ` M ) )