This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )