Theorem isgrpi

Description: Properties that determine a group. N (negative) is normally dependent on x i.e. read it as N ( x ) . (Contributed by NM, 3-Sep-2011)

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

Proof

Step	Hyp	Ref	Expression
1		isgrpi.b	|- B = ( Base ` G )
2		isgrpi.p	|- .+ = ( +g ` G )
3		isgrpi.c	|- ( ( x e. B /\ y e. B ) -> ( x .+ y ) e. B )
4		isgrpi.a	|- ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
5		isgrpi.z	|- .0. e. B
6		isgrpi.i	|- ( x e. B -> ( .0. .+ x ) = x )
7		isgrpi.n	|- ( x e. B -> N e. B )
8		isgrpi.j	|- ( x e. B -> ( N .+ x ) = .0. )
9	1	a1i	|- ( T. -> B = ( Base ` G ) )
10	2	a1i	|- ( T. -> .+ = ( +g ` G ) )
11	3	3adant1	|- ( ( T. /\ x e. B /\ y e. B ) -> ( x .+ y ) e. B )
12	4	adantl	|- ( ( T. /\ ( x e. B /\ y e. B /\ z e. B ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
13	5	a1i	|- ( T. -> .0. e. B )
14	6	adantl	|- ( ( T. /\ x e. B ) -> ( .0. .+ x ) = x )
15	7	adantl	|- ( ( T. /\ x e. B ) -> N e. B )
16	8	adantl	|- ( ( T. /\ x e. B ) -> ( N .+ x ) = .0. )
17	9 10 11 12 13 14 15 16	isgrpd	|- ( T. -> G e. Grp )
18	17	mptru	|- G e. Grp