Step |
Hyp |
Ref |
Expression |
1 |
|
submacs.b |
|- B = ( Base ` G ) |
2 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
3 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
4 |
1 2 3
|
issubm |
|- ( G e. Mnd -> ( s e. ( SubMnd ` G ) <-> ( s C_ B /\ ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) ) ) |
5 |
|
velpw |
|- ( s e. ~P B <-> s C_ B ) |
6 |
5
|
anbi1i |
|- ( ( s e. ~P B /\ ( ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) ) <-> ( s C_ B /\ ( ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) ) ) |
7 |
|
3anass |
|- ( ( s C_ B /\ ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) <-> ( s C_ B /\ ( ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) ) ) |
8 |
6 7
|
bitr4i |
|- ( ( s e. ~P B /\ ( ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) ) <-> ( s C_ B /\ ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) ) |
9 |
4 8
|
bitr4di |
|- ( G e. Mnd -> ( s e. ( SubMnd ` G ) <-> ( s e. ~P B /\ ( ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) ) ) ) |
10 |
9
|
abbi2dv |
|- ( G e. Mnd -> ( SubMnd ` G ) = { s | ( s e. ~P B /\ ( ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) ) } ) |
11 |
|
df-rab |
|- { s e. ~P B | ( ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) } = { s | ( s e. ~P B /\ ( ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) ) } |
12 |
10 11
|
eqtr4di |
|- ( G e. Mnd -> ( SubMnd ` G ) = { s e. ~P B | ( ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) } ) |
13 |
|
inrab |
|- ( { s e. ~P B | ( 0g ` G ) e. s } i^i { s e. ~P B | A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s } ) = { s e. ~P B | ( ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) } |
14 |
1
|
fvexi |
|- B e. _V |
15 |
|
mreacs |
|- ( B e. _V -> ( ACS ` B ) e. ( Moore ` ~P B ) ) |
16 |
14 15
|
mp1i |
|- ( G e. Mnd -> ( ACS ` B ) e. ( Moore ` ~P B ) ) |
17 |
1 2
|
mndidcl |
|- ( G e. Mnd -> ( 0g ` G ) e. B ) |
18 |
|
acsfn0 |
|- ( ( B e. _V /\ ( 0g ` G ) e. B ) -> { s e. ~P B | ( 0g ` G ) e. s } e. ( ACS ` B ) ) |
19 |
14 17 18
|
sylancr |
|- ( G e. Mnd -> { s e. ~P B | ( 0g ` G ) e. s } e. ( ACS ` B ) ) |
20 |
1 3
|
mndcl |
|- ( ( G e. Mnd /\ x e. B /\ y e. B ) -> ( x ( +g ` G ) y ) e. B ) |
21 |
20
|
3expb |
|- ( ( G e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` G ) y ) e. B ) |
22 |
21
|
ralrimivva |
|- ( G e. Mnd -> A. x e. B A. y e. B ( x ( +g ` G ) y ) e. B ) |
23 |
|
acsfn2 |
|- ( ( B e. _V /\ A. x e. B A. y e. B ( x ( +g ` G ) y ) e. B ) -> { s e. ~P B | A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s } e. ( ACS ` B ) ) |
24 |
14 22 23
|
sylancr |
|- ( G e. Mnd -> { s e. ~P B | A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s } e. ( ACS ` B ) ) |
25 |
|
mreincl |
|- ( ( ( ACS ` B ) e. ( Moore ` ~P B ) /\ { s e. ~P B | ( 0g ` G ) e. s } e. ( ACS ` B ) /\ { s e. ~P B | A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s } e. ( ACS ` B ) ) -> ( { s e. ~P B | ( 0g ` G ) e. s } i^i { s e. ~P B | A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s } ) e. ( ACS ` B ) ) |
26 |
16 19 24 25
|
syl3anc |
|- ( G e. Mnd -> ( { s e. ~P B | ( 0g ` G ) e. s } i^i { s e. ~P B | A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s } ) e. ( ACS ` B ) ) |
27 |
13 26
|
eqeltrrid |
|- ( G e. Mnd -> { s e. ~P B | ( ( 0g ` G ) e. s /\ A. x e. s A. y e. s ( x ( +g ` G ) y ) e. s ) } e. ( ACS ` B ) ) |
28 |
12 27
|
eqeltrd |
|- ( G e. Mnd -> ( SubMnd ` G ) e. ( ACS ` B ) ) |