Metamath Proof Explorer

Theorem ismnddef

Description: The predicate "is a monoid", corresponding 1-to-1 to the definition. (Contributed by FL, 2-Nov-2009) (Revised by AV, 1-Feb-2020)

Ref Expression
Hypotheses ismnddef.b 
|- B = ( Base ` G )
ismnddef.p 
|- .+ = ( +g ` G )
Assertion ismnddef 
|- ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )

Proof

Step Hyp Ref Expression
1 ismnddef.b 
 |-  B = ( Base ` G )
2 ismnddef.p 
 |-  .+ = ( +g ` G )
3 fvex 
 |-  ( Base ` g ) e. _V
4 fvex 
 |-  ( +g ` g ) e. _V
5 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
6 5 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = B )
7 6 eqeq2d 
 |-  ( g = G -> ( b = ( Base ` g ) <-> b = B ) )
8 fveq2 
 |-  ( g = G -> ( +g ` g ) = ( +g ` G ) )
9 8 2 eqtr4di 
 |-  ( g = G -> ( +g ` g ) = .+ )
10 9 eqeq2d 
 |-  ( g = G -> ( p = ( +g ` g ) <-> p = .+ ) )
11 7 10 anbi12d 
 |-  ( g = G -> ( ( b = ( Base ` g ) /\ p = ( +g ` g ) ) <-> ( b = B /\ p = .+ ) ) )
12 simpl 
 |-  ( ( b = B /\ p = .+ ) -> b = B )
13 oveq 
 |-  ( p = .+ -> ( e p a ) = ( e .+ a ) )
14 13 eqeq1d 
 |-  ( p = .+ -> ( ( e p a ) = a <-> ( e .+ a ) = a ) )
15 oveq 
 |-  ( p = .+ -> ( a p e ) = ( a .+ e ) )
16 15 eqeq1d 
 |-  ( p = .+ -> ( ( a p e ) = a <-> ( a .+ e ) = a ) )
17 14 16 anbi12d 
 |-  ( p = .+ -> ( ( ( e p a ) = a /\ ( a p e ) = a ) <-> ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
18 17 adantl 
 |-  ( ( b = B /\ p = .+ ) -> ( ( ( e p a ) = a /\ ( a p e ) = a ) <-> ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
19 12 18 raleqbidv 
 |-  ( ( b = B /\ p = .+ ) -> ( A. a e. b ( ( e p a ) = a /\ ( a p e ) = a ) <-> A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
20 12 19 rexeqbidv 
 |-  ( ( b = B /\ p = .+ ) -> ( E. e e. b A. a e. b ( ( e p a ) = a /\ ( a p e ) = a ) <-> E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
21 11 20 syl6bi 
 |-  ( g = G -> ( ( b = ( Base ` g ) /\ p = ( +g ` g ) ) -> ( E. e e. b A. a e. b ( ( e p a ) = a /\ ( a p e ) = a ) <-> E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) ) )
22 3 4 21 sbc2iedv 
 |-  ( g = G -> ( [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. a e. b ( ( e p a ) = a /\ ( a p e ) = a ) <-> E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )
23 df-mnd 
 |-  Mnd = { g e. Smgrp | [. ( Base ` g ) / b ]. [. ( +g ` g ) / p ]. E. e e. b A. a e. b ( ( e p a ) = a /\ ( a p e ) = a ) }
24 22 23 elrab2 
 |-  ( G e. Mnd <-> ( G e. Smgrp /\ E. e e. B A. a e. B ( ( e .+ a ) = a /\ ( a .+ e ) = a ) ) )