Theorem isgrpde

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

	Ref	Expression
Hypotheses	isgrpd.b	|- ( ph -> B = ( Base ` G ) )
	isgrpd.p	|- ( ph -> .+ = ( +g ` G ) )
	isgrpd.c	|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
	isgrpd.a	|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
	isgrpd.z	|- ( ph -> .0. e. B )
	isgrpd.i	|- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )
	isgrpde.n	|- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = .0. )
Assertion	isgrpde	|- ( ph -> G e. Grp )

Proof

Step	Hyp	Ref	Expression
1		isgrpd.b	|- ( ph -> B = ( Base ` G ) )
2		isgrpd.p	|- ( ph -> .+ = ( +g ` G ) )
3		isgrpd.c	|- ( ( ph /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
4		isgrpd.a	|- ( ( ph /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
5		isgrpd.z	|- ( ph -> .0. e. B )
6		isgrpd.i	|- ( ( ph /\ x e. B ) -> ( .0. .+ x ) = x )
7		isgrpde.n	|- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = .0. )
8	3 5 6 4 7	grpridd	|- ( ( ph /\ x e. B ) -> ( x .+ .0. ) = x )
9	1 2 5 6 8	grpidd	|- ( ph -> .0. = ( 0g ` G ) )
10	1 2 3 4 5 6 8	ismndd	|- ( ph -> G e. Mnd )
11	1 2 9 10 7	isgrpd2e	|- ( ph -> G e. Grp )