Step |
Hyp |
Ref |
Expression |
1 |
|
issubmgm.b |
|- B = ( Base ` M ) |
2 |
|
issubmgm.p |
|- .+ = ( +g ` M ) |
3 |
|
fveq2 |
|- ( m = M -> ( Base ` m ) = ( Base ` M ) ) |
4 |
3
|
pweqd |
|- ( m = M -> ~P ( Base ` m ) = ~P ( Base ` M ) ) |
5 |
|
fveq2 |
|- ( m = M -> ( +g ` m ) = ( +g ` M ) ) |
6 |
5
|
oveqd |
|- ( m = M -> ( x ( +g ` m ) y ) = ( x ( +g ` M ) y ) ) |
7 |
6
|
eleq1d |
|- ( m = M -> ( ( x ( +g ` m ) y ) e. t <-> ( x ( +g ` M ) y ) e. t ) ) |
8 |
7
|
2ralbidv |
|- ( m = M -> ( A. x e. t A. y e. t ( x ( +g ` m ) y ) e. t <-> A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t ) ) |
9 |
4 8
|
rabeqbidv |
|- ( m = M -> { t e. ~P ( Base ` m ) | A. x e. t A. y e. t ( x ( +g ` m ) y ) e. t } = { t e. ~P ( Base ` M ) | A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t } ) |
10 |
|
df-submgm |
|- SubMgm = ( m e. Mgm |-> { t e. ~P ( Base ` m ) | A. x e. t A. y e. t ( x ( +g ` m ) y ) e. t } ) |
11 |
|
fvex |
|- ( Base ` M ) e. _V |
12 |
11
|
pwex |
|- ~P ( Base ` M ) e. _V |
13 |
12
|
rabex |
|- { t e. ~P ( Base ` M ) | A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t } e. _V |
14 |
9 10 13
|
fvmpt |
|- ( M e. Mgm -> ( SubMgm ` M ) = { t e. ~P ( Base ` M ) | A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t } ) |
15 |
14
|
eleq2d |
|- ( M e. Mgm -> ( S e. ( SubMgm ` M ) <-> S e. { t e. ~P ( Base ` M ) | A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t } ) ) |
16 |
11
|
elpw2 |
|- ( S e. ~P ( Base ` M ) <-> S C_ ( Base ` M ) ) |
17 |
16
|
anbi1i |
|- ( ( S e. ~P ( Base ` M ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) <-> ( S C_ ( Base ` M ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) |
18 |
|
eleq2 |
|- ( t = S -> ( ( x ( +g ` M ) y ) e. t <-> ( x ( +g ` M ) y ) e. S ) ) |
19 |
18
|
raleqbi1dv |
|- ( t = S -> ( A. y e. t ( x ( +g ` M ) y ) e. t <-> A. y e. S ( x ( +g ` M ) y ) e. S ) ) |
20 |
19
|
raleqbi1dv |
|- ( t = S -> ( A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t <-> A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) |
21 |
20
|
elrab |
|- ( S e. { t e. ~P ( Base ` M ) | A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t } <-> ( S e. ~P ( Base ` M ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) |
22 |
1
|
sseq2i |
|- ( S C_ B <-> S C_ ( Base ` M ) ) |
23 |
2
|
oveqi |
|- ( x .+ y ) = ( x ( +g ` M ) y ) |
24 |
23
|
eleq1i |
|- ( ( x .+ y ) e. S <-> ( x ( +g ` M ) y ) e. S ) |
25 |
24
|
2ralbii |
|- ( A. x e. S A. y e. S ( x .+ y ) e. S <-> A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) |
26 |
22 25
|
anbi12i |
|- ( ( S C_ B /\ A. x e. S A. y e. S ( x .+ y ) e. S ) <-> ( S C_ ( Base ` M ) /\ A. x e. S A. y e. S ( x ( +g ` M ) y ) e. S ) ) |
27 |
17 21 26
|
3bitr4i |
|- ( S e. { t e. ~P ( Base ` M ) | A. x e. t A. y e. t ( x ( +g ` M ) y ) e. t } <-> ( S C_ B /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) |
28 |
15 27
|
bitrdi |
|- ( M e. Mgm -> ( S e. ( SubMgm ` M ) <-> ( S C_ B /\ A. x e. S A. y e. S ( x .+ y ) e. S ) ) ) |