# Metamath Proof Explorer

## Theorem ismgm

Description: The predicate "is a magma". (Contributed by FL, 2-Nov-2009) (Revised by AV, 6-Jan-2020)

Ref Expression
Hypotheses ismgm.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
ismgm.o No typesetting found for |- .o. = ( +g  M ) with typecode |-
Assertion ismgm Could not format assertion : No typesetting found for |- ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-

### Proof

Step Hyp Ref Expression
1 ismgm.b ${⊢}{B}={\mathrm{Base}}_{{M}}$
2 ismgm.o Could not format .o. = ( +g  M ) : No typesetting found for |- .o. = ( +g  M ) with typecode |-
3 fvexd ${⊢}{m}={M}\to {\mathrm{Base}}_{{m}}\in \mathrm{V}$
4 fveq2 ${⊢}{m}={M}\to {\mathrm{Base}}_{{m}}={\mathrm{Base}}_{{M}}$
5 4 1 eqtr4di ${⊢}{m}={M}\to {\mathrm{Base}}_{{m}}={B}$
6 fvexd ${⊢}\left({m}={M}\wedge {b}={B}\right)\to {+}_{{m}}\in \mathrm{V}$
7 fveq2 ${⊢}{m}={M}\to {+}_{{m}}={+}_{{M}}$
8 7 adantr ${⊢}\left({m}={M}\wedge {b}={B}\right)\to {+}_{{m}}={+}_{{M}}$
9 8 2 eqtr4di Could not format ( ( m = M /\ b = B ) -> ( +g  m ) = .o. ) : No typesetting found for |- ( ( m = M /\ b = B ) -> ( +g  m ) = .o. ) with typecode |-
10 simplr Could not format ( ( ( m = M /\ b = B ) /\ o = .o. ) -> b = B ) : No typesetting found for |- ( ( ( m = M /\ b = B ) /\ o = .o. ) -> b = B ) with typecode |-
11 oveq Could not format ( o = .o. -> ( x o y ) = ( x .o. y ) ) : No typesetting found for |- ( o = .o. -> ( x o y ) = ( x .o. y ) ) with typecode |-
12 11 adantl Could not format ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( x o y ) = ( x .o. y ) ) : No typesetting found for |- ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( x o y ) = ( x .o. y ) ) with typecode |-
13 12 10 eleq12d Could not format ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( ( x o y ) e. b <-> ( x .o. y ) e. B ) ) : No typesetting found for |- ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( ( x o y ) e. b <-> ( x .o. y ) e. B ) ) with typecode |-
14 10 13 raleqbidv Could not format ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( A. y e. b ( x o y ) e. b <-> A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( A. y e. b ( x o y ) e. b <-> A. y e. B ( x .o. y ) e. B ) ) with typecode |-
15 10 14 raleqbidv Could not format ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( A. x e. b A. y e. b ( x o y ) e. b <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( A. x e. b A. y e. b ( x o y ) e. b <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-
16 6 9 15 sbcied2 Could not format ( ( m = M /\ b = B ) -> ( [. ( +g  m ) / o ]. A. x e. b A. y e. b ( x o y ) e. b <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( ( m = M /\ b = B ) -> ( [. ( +g  m ) / o ]. A. x e. b A. y e. b ( x o y ) e. b <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-
17 3 5 16 sbcied2 Could not format ( m = M -> ( [. ( Base  m ) / b ]. [. ( +g  m ) / o ]. A. x e. b A. y e. b ( x o y ) e. b <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( m = M -> ( [. ( Base  m ) / b ]. [. ( +g ` m ) / o ]. A. x e. b A. y e. b ( x o y ) e. b <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-
18 df-mgm
19 17 18 elab2g Could not format ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) : No typesetting found for |- ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) ) with typecode |-