This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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. ) )