Theorem isgrpd

Description: Deduce a group from its properties. Unlike isgrpd2 , this one goes straight from the base properties rather than going through Mnd . N (negative) is normally dependent on x i.e. read it as N ( x ) . (Contributed by NM, 6-Jun-2013) (Revised by Mario Carneiro, 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 )
	isgrpd.n	|- ( ( ph /\ x e. B ) -> N e. B )
	isgrpd.j	|- ( ( ph /\ x e. B ) -> ( N .+ x ) = .0. )
Assertion	isgrpd	|- ( 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		isgrpd.n	|- ( ( ph /\ x e. B ) -> N e. B )
8		isgrpd.j	|- ( ( ph /\ x e. B ) -> ( N .+ x ) = .0. )
9		oveq1	|- ( y = N -> ( y .+ x ) = ( N .+ x ) )
10	9	eqeq1d	|- ( y = N -> ( ( y .+ x ) = .0. <-> ( N .+ x ) = .0. ) )
11	10	rspcev	|- ( ( N e. B /\ ( N .+ x ) = .0. ) -> E. y e. B ( y .+ x ) = .0. )
12	7 8 11	syl2anc	|- ( ( ph /\ x e. B ) -> E. y e. B ( y .+ x ) = .0. )
13	1 2 3 4 5 6 12	isgrpde	|- ( ph -> G e. Grp )