Metamath Proof Explorer


Theorem ismgmALT

Description: The predicate "is a magma". (Contributed by AV, 16-Jan-2020) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses ismgmALT.b B=BaseM
ismgmALT.o No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion ismgmALT Could not format assertion : No typesetting found for |- ( M e. V -> ( M e. MgmALT <-> .o. clLaw B ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 ismgmALT.b B=BaseM
2 ismgmALT.o Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |-
3 fveq2 m=M+m=+M
4 3 2 eqtr4di Could not format ( m = M -> ( +g ` m ) = .o. ) : No typesetting found for |- ( m = M -> ( +g ` m ) = .o. ) with typecode |-
5 fveq2 m=MBasem=BaseM
6 5 1 eqtr4di m=MBasem=B
7 4 6 breq12d Could not format ( m = M -> ( ( +g ` m ) clLaw ( Base ` m ) <-> .o. clLaw B ) ) : No typesetting found for |- ( m = M -> ( ( +g ` m ) clLaw ( Base ` m ) <-> .o. clLaw B ) ) with typecode |-
8 df-mgm2 MgmALT=m|+mclLawBasem
9 7 8 elab2g Could not format ( M e. V -> ( M e. MgmALT <-> .o. clLaw B ) ) : No typesetting found for |- ( M e. V -> ( M e. MgmALT <-> .o. clLaw B ) ) with typecode |-