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