Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Base ` M ) = ( Base ` M ) |
2 |
|
eqid |
|- ( +g ` M ) = ( +g ` M ) |
3 |
1 2
|
ismgmALT |
|- ( M e. MgmALT -> ( M e. MgmALT <-> ( +g ` M ) clLaw ( Base ` M ) ) ) |
4 |
|
fvex |
|- ( +g ` M ) e. _V |
5 |
|
fvex |
|- ( Base ` M ) e. _V |
6 |
|
iscllaw |
|- ( ( ( +g ` M ) e. _V /\ ( Base ` M ) e. _V ) -> ( ( +g ` M ) clLaw ( Base ` M ) <-> A. x e. ( Base ` M ) A. y e. ( Base ` M ) ( x ( +g ` M ) y ) e. ( Base ` M ) ) ) |
7 |
4 5 6
|
mp2an |
|- ( ( +g ` M ) clLaw ( Base ` M ) <-> A. x e. ( Base ` M ) A. y e. ( Base ` M ) ( x ( +g ` M ) y ) e. ( Base ` M ) ) |
8 |
1 2
|
ismgm |
|- ( M e. MgmALT -> ( M e. Mgm <-> A. x e. ( Base ` M ) A. y e. ( Base ` M ) ( x ( +g ` M ) y ) e. ( Base ` M ) ) ) |
9 |
8
|
biimprd |
|- ( M e. MgmALT -> ( A. x e. ( Base ` M ) A. y e. ( Base ` M ) ( x ( +g ` M ) y ) e. ( Base ` M ) -> M e. Mgm ) ) |
10 |
7 9
|
syl5bi |
|- ( M e. MgmALT -> ( ( +g ` M ) clLaw ( Base ` M ) -> M e. Mgm ) ) |
11 |
3 10
|
sylbid |
|- ( M e. MgmALT -> ( M e. MgmALT -> M e. Mgm ) ) |
12 |
11
|
pm2.43i |
|- ( M e. MgmALT -> M e. Mgm ) |
13 |
|
mgmplusgiopALT |
|- ( M e. Mgm -> ( +g ` M ) clLaw ( Base ` M ) ) |
14 |
1 2
|
ismgmALT |
|- ( M e. Mgm -> ( M e. MgmALT <-> ( +g ` M ) clLaw ( Base ` M ) ) ) |
15 |
13 14
|
mpbird |
|- ( M e. Mgm -> M e. MgmALT ) |
16 |
12 15
|
impbii |
|- ( M e. MgmALT <-> M e. Mgm ) |