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 |
|
smndex1mgm.b |
|- B = ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) |
6 |
|
smndex1mgm.s |
|- S = ( M |`s B ) |
7 |
1 2 3 4 5 6
|
smndex1mgm |
|- S e. Mgm |
8 |
|
eqid |
|- ( Base ` S ) = ( Base ` S ) |
9 |
|
eqid |
|- ( +g ` S ) = ( +g ` S ) |
10 |
8 9
|
mgmcl |
|- ( ( S e. Mgm /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) ) |
11 |
7 10
|
mp3an1 |
|- ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` S ) y ) e. ( Base ` S ) ) |
12 |
|
snex |
|- { I } e. _V |
13 |
|
ovex |
|- ( 0 ..^ N ) e. _V |
14 |
|
snex |
|- { ( G ` n ) } e. _V |
15 |
13 14
|
iunex |
|- U_ n e. ( 0 ..^ N ) { ( G ` n ) } e. _V |
16 |
12 15
|
unex |
|- ( { I } u. U_ n e. ( 0 ..^ N ) { ( G ` n ) } ) e. _V |
17 |
5 16
|
eqeltri |
|- B e. _V |
18 |
|
eqid |
|- ( +g ` M ) = ( +g ` M ) |
19 |
6 18
|
ressplusg |
|- ( B e. _V -> ( +g ` M ) = ( +g ` S ) ) |
20 |
17 19
|
ax-mp |
|- ( +g ` M ) = ( +g ` S ) |
21 |
20
|
eqcomi |
|- ( +g ` S ) = ( +g ` M ) |
22 |
21
|
oveqi |
|- ( x ( +g ` S ) y ) = ( x ( +g ` M ) y ) |
23 |
1 2 3 4 5 6
|
smndex1bas |
|- ( Base ` S ) = B |
24 |
1 2 3 4 5
|
smndex1basss |
|- B C_ ( Base ` M ) |
25 |
23 24
|
eqsstri |
|- ( Base ` S ) C_ ( Base ` M ) |
26 |
|
ssel |
|- ( ( Base ` S ) C_ ( Base ` M ) -> ( x e. ( Base ` S ) -> x e. ( Base ` M ) ) ) |
27 |
|
ssel |
|- ( ( Base ` S ) C_ ( Base ` M ) -> ( y e. ( Base ` S ) -> y e. ( Base ` M ) ) ) |
28 |
26 27
|
anim12d |
|- ( ( Base ` S ) C_ ( Base ` M ) -> ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) ) |
29 |
25 28
|
ax-mp |
|- ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) ) |
30 |
|
eqid |
|- ( Base ` M ) = ( Base ` M ) |
31 |
1 30 18
|
efmndov |
|- ( ( x e. ( Base ` M ) /\ y e. ( Base ` M ) ) -> ( x ( +g ` M ) y ) = ( x o. y ) ) |
32 |
29 31
|
syl |
|- ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` M ) y ) = ( x o. y ) ) |
33 |
22 32
|
syl5eq |
|- ( ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( x ( +g ` S ) y ) = ( x o. y ) ) |
34 |
11 33
|
symggrplem |
|- ( ( a e. ( Base ` S ) /\ b e. ( Base ` S ) /\ c e. ( Base ` S ) ) -> ( ( a ( +g ` S ) b ) ( +g ` S ) c ) = ( a ( +g ` S ) ( b ( +g ` S ) c ) ) ) |
35 |
34
|
rgen3 |
|- A. a e. ( Base ` S ) A. b e. ( Base ` S ) A. c e. ( Base ` S ) ( ( a ( +g ` S ) b ) ( +g ` S ) c ) = ( a ( +g ` S ) ( b ( +g ` S ) c ) ) |
36 |
8 9
|
issgrp |
|- ( S e. Smgrp <-> ( S e. Mgm /\ A. a e. ( Base ` S ) A. b e. ( Base ` S ) A. c e. ( Base ` S ) ( ( a ( +g ` S ) b ) ( +g ` S ) c ) = ( a ( +g ` S ) ( b ( +g ` S ) c ) ) ) ) |
37 |
7 35 36
|
mpbir2an |
|- S e. Smgrp |