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 = ( Base ` M )
ismgm.o 
|- .o. = ( +g ` M )
Assertion ismgm 
|- ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )

Proof

Step Hyp Ref Expression
1 ismgm.b 
 |-  B = ( Base ` M )
2 ismgm.o 
 |-  .o. = ( +g ` M )
3 fvexd 
 |-  ( m = M -> ( Base ` m ) e. _V )
4 fveq2 
 |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )
5 4 1 eqtr4di 
 |-  ( m = M -> ( Base ` m ) = B )
6 fvexd 
 |-  ( ( m = M /\ b = B ) -> ( +g ` m ) e. _V )
7 fveq2 
 |-  ( m = M -> ( +g ` m ) = ( +g ` M ) )
8 7 adantr 
 |-  ( ( m = M /\ b = B ) -> ( +g ` m ) = ( +g ` M ) )
9 8 2 eqtr4di 
 |-  ( ( m = M /\ b = B ) -> ( +g ` m ) = .o. )
10 simplr 
 |-  ( ( ( m = M /\ b = B ) /\ o = .o. ) -> b = B )
11 oveq 
 |-  ( o = .o. -> ( x o y ) = ( x .o. y ) )
12 11 adantl 
 |-  ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( x o y ) = ( x .o. y ) )
13 12 10 eleq12d 
 |-  ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( ( x o y ) e. b <-> ( x .o. y ) e. B ) )
14 10 13 raleqbidv 
 |-  ( ( ( m = M /\ b = B ) /\ o = .o. ) -> ( A. y e. b ( x o y ) e. b <-> A. y e. B ( x .o. y ) e. B ) )
15 10 14 raleqbidv 
 |-  ( ( ( 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 ) )
16 6 9 15 sbcied2 
 |-  ( ( 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 ) )
17 3 5 16 sbcied2 
 |-  ( 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 ) )
18 df-mgm 
 |-  Mgm = { m | [. ( Base ` m ) / b ]. [. ( +g ` m ) / o ]. A. x e. b A. y e. b ( x o y ) e. b }
19 17 18 elab2g 
 |-  ( M e. V -> ( M e. Mgm <-> A. x e. B A. y e. B ( x .o. y ) e. B ) )