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 
|- .o. = ( +g ` M )
Assertion iscsgrpALT 
|- ( M e. CSGrpALT <-> ( M e. SGrpALT /\ .o. comLaw B ) )

Proof

Step Hyp Ref Expression
1 ismgmALT.b 
 |-  B = ( Base ` M )
2 ismgmALT.o 
 |-  .o. = ( +g ` M )
3 fveq2 
 |-  ( m = M -> ( +g ` m ) = ( +g ` M ) )
4 fveq2 
 |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )
5 3 4 breq12d 
 |-  ( m = M -> ( ( +g ` m ) comLaw ( Base ` m ) <-> ( +g ` M ) comLaw ( Base ` M ) ) )
6 2 1 breq12i 
 |-  ( .o. comLaw B <-> ( +g ` M ) comLaw ( Base ` M ) )
7 5 6 bitr4di 
 |-  ( m = M -> ( ( +g ` m ) comLaw ( Base ` m ) <-> .o. comLaw B ) )
8 df-csgrp2 
 |-  CSGrpALT = { m e. SGrpALT | ( +g ` m ) comLaw ( Base ` m ) }
9 7 8 elrab2 
 |-  ( M e. CSGrpALT <-> ( M e. SGrpALT /\ .o. comLaw B ) )