Step |
Hyp |
Ref |
Expression |
1 |
|
ismgmALT.b |
|
2 |
|
ismgmALT.o |
Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |- |
3 |
|
fveq2 |
|
4 |
|
fveq2 |
|
5 |
3 4
|
breq12d |
|
6 |
2 1
|
breq12i |
Could not format ( .o. comLaw B <-> ( +g ` M ) comLaw ( Base ` M ) ) : No typesetting found for |- ( .o. comLaw B <-> ( +g ` M ) comLaw ( Base ` M ) ) with typecode |- |
7 |
5 6
|
bitr4di |
Could not format ( m = M -> ( ( +g ` m ) comLaw ( Base ` m ) <-> .o. comLaw B ) ) : No typesetting found for |- ( m = M -> ( ( +g ` m ) comLaw ( Base ` m ) <-> .o. comLaw B ) ) with typecode |- |
8 |
|
df-csgrp2 |
|
9 |
7 8
|
elrab2 |
Could not format ( M e. CSGrpALT <-> ( M e. SGrpALT /\ .o. comLaw B ) ) : No typesetting found for |- ( M e. CSGrpALT <-> ( M e. SGrpALT /\ .o. comLaw B ) ) with typecode |- |