Theorem isgrpd2e

Description: Deduce a group from its properties. In this version of isgrpd2 , we don't assume there is an expression for the inverse of x . (Contributed by NM, 10-Aug-2013)

	Ref	Expression
Hypotheses	isgrpd2.b	|- ( ph -> B = ( Base ` G ) )
	isgrpd2.p	|- ( ph -> .+ = ( +g ` G ) )
	isgrpd2.z	|- ( ph -> .0. = ( 0g ` G ) )
	isgrpd2.g	|- ( ph -> G e. Mnd )
	isgrpd2e.n	|- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = .0. )
Assertion	isgrpd2e	|- ( ph -> G e. Grp )

Proof

Step	Hyp	Ref	Expression
1		isgrpd2.b	|- ( ph -> B = ( Base ` G ) )
2		isgrpd2.p	|- ( ph -> .+ = ( +g ` G ) )
3		isgrpd2.z	|- ( ph -> .0. = ( 0g ` G ) )
4		isgrpd2.g	|- ( ph -> G e. Mnd )
5		isgrpd2e.n	|- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = .0. )
6	5	ralrimiva	|- ( ph -> A. x e. B E. y e. B ( y .+ x ) = .0. )
7	2	oveqd	|- ( ph -> ( y .+ x ) = ( y ( +g ` G ) x ) )
8	7 3	eqeq12d	|- ( ph -> ( ( y .+ x ) = .0. <-> ( y ( +g ` G ) x ) = ( 0g ` G ) ) )
9	1 8	rexeqbidv	|- ( ph -> ( E. y e. B ( y .+ x ) = .0. <-> E. y e. ( Base ` G ) ( y ( +g ` G ) x ) = ( 0g ` G ) ) )
10	1 9	raleqbidv	|- ( ph -> ( A. x e. B E. y e. B ( y .+ x ) = .0. <-> A. x e. ( Base ` G ) E. y e. ( Base ` G ) ( y ( +g ` G ) x ) = ( 0g ` G ) ) )
11	6 10	mpbid	|- ( ph -> A. x e. ( Base ` G ) E. y e. ( Base ` G ) ( y ( +g ` G ) x ) = ( 0g ` G ) )
12		eqid	|- ( Base ` G ) = ( Base ` G )
13		eqid	|- ( +g ` G ) = ( +g ` G )
14		eqid	|- ( 0g ` G ) = ( 0g ` G )
15	12 13 14	isgrp	|- ( G e. Grp <-> ( G e. Mnd /\ A. x e. ( Base ` G ) E. y e. ( Base ` G ) ( y ( +g ` G ) x ) = ( 0g ` G ) ) )
16	4 11 15	sylanbrc	|- ( ph -> G e. Grp )