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 |
|
eqid |
|- ( x e. NN0 |-> ( x mod N ) ) = ( x e. NN0 |-> ( x mod N ) ) |
5 |
|
nn0z |
|- ( x e. NN0 -> x e. ZZ ) |
6 |
2
|
a1i |
|- ( x e. NN0 -> N e. NN ) |
7 |
5 6
|
zmodcld |
|- ( x e. NN0 -> ( x mod N ) e. NN0 ) |
8 |
4 7
|
fmpti |
|- ( x e. NN0 |-> ( x mod N ) ) : NN0 --> NN0 |
9 |
|
nn0ex |
|- NN0 e. _V |
10 |
9 9
|
elmap |
|- ( ( x e. NN0 |-> ( x mod N ) ) e. ( NN0 ^m NN0 ) <-> ( x e. NN0 |-> ( x mod N ) ) : NN0 --> NN0 ) |
11 |
8 10
|
mpbir |
|- ( x e. NN0 |-> ( x mod N ) ) e. ( NN0 ^m NN0 ) |
12 |
|
eqid |
|- ( Base ` M ) = ( Base ` M ) |
13 |
1 12
|
efmndbas |
|- ( Base ` M ) = ( NN0 ^m NN0 ) |
14 |
11 3 13
|
3eltr4i |
|- I e. ( Base ` M ) |