Metamath Proof Explorer


Theorem mgm2mgm

Description: Equivalence of the two definitions of a magma. (Contributed by AV, 16-Jan-2020)

Ref Expression
Assertion mgm2mgm
|- ( M e. MgmALT <-> M e. Mgm )

Proof

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 )