Metamath Proof Explorer


Theorem isgrp

Description: The predicate "is a group." (This theorem demonstrates the use of symbols as variable names, first proposed by FL in 2010.) (Contributed by NM, 17-Oct-2012) (Revised by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypotheses isgrp.b
|- B = ( Base ` G )
isgrp.p
|- .+ = ( +g ` G )
isgrp.z
|- .0. = ( 0g ` G )
Assertion isgrp
|- ( G e. Grp <-> ( G e. Mnd /\ A. a e. B E. m e. B ( m .+ a ) = .0. ) )

Proof

Step Hyp Ref Expression
1 isgrp.b
 |-  B = ( Base ` G )
2 isgrp.p
 |-  .+ = ( +g ` G )
3 isgrp.z
 |-  .0. = ( 0g ` G )
4 fveq2
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
5 4 1 eqtr4di
 |-  ( g = G -> ( Base ` g ) = B )
6 fveq2
 |-  ( g = G -> ( +g ` g ) = ( +g ` G ) )
7 6 2 eqtr4di
 |-  ( g = G -> ( +g ` g ) = .+ )
8 7 oveqd
 |-  ( g = G -> ( m ( +g ` g ) a ) = ( m .+ a ) )
9 fveq2
 |-  ( g = G -> ( 0g ` g ) = ( 0g ` G ) )
10 9 3 eqtr4di
 |-  ( g = G -> ( 0g ` g ) = .0. )
11 8 10 eqeq12d
 |-  ( g = G -> ( ( m ( +g ` g ) a ) = ( 0g ` g ) <-> ( m .+ a ) = .0. ) )
12 5 11 rexeqbidv
 |-  ( g = G -> ( E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) <-> E. m e. B ( m .+ a ) = .0. ) )
13 5 12 raleqbidv
 |-  ( g = G -> ( A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) <-> A. a e. B E. m e. B ( m .+ a ) = .0. ) )
14 df-grp
 |-  Grp = { g e. Mnd | A. a e. ( Base ` g ) E. m e. ( Base ` g ) ( m ( +g ` g ) a ) = ( 0g ` g ) }
15 13 14 elrab2
 |-  ( G e. Grp <-> ( G e. Mnd /\ A. a e. B E. m e. B ( m .+ a ) = .0. ) )