Metamath Proof Explorer


Theorem iscsgrpALT

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

Ref Expression
Hypotheses ismgmALT.b B = Base M
ismgmALT.o No typesetting found for |- .o. = ( +g ` M ) with typecode |-
Assertion iscsgrpALT Could not format assertion : No typesetting found for |- ( M e. CSGrpALT <-> ( M e. SGrpALT /\ .o. comLaw B ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 ismgmALT.b B = Base M
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 fveq2 m = M Base m = Base M
5 3 4 breq12d m = M + m comLaw Base m + M comLaw Base M
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 CSGrpALT = m SGrpALT | + m comLaw Base m
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 |-