Theorem isgrpix

Description: Properties that determine a group. Read N as N ( x ) . Note: This theorem has hard-coded structure indices for demonstration purposes. It is not intended for general use. (New usage is discouraged.) (Contributed by NM, 4-Sep-2011)

	Ref	Expression
Hypotheses	isgrpix.a	|- B e. _V
	isgrpix.b	|- .+ e. _V
	isgrpix.g	|- G = { <. 1 , B >. , <. 2 , .+ >. }
	isgrpix.2	|- ( ( x e. B /\ y e. B ) -> ( x .+ y ) e. B )
	isgrpix.3	|- ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
	isgrpix.z	|- .0. e. B
	isgrpix.5	|- ( x e. B -> ( .0. .+ x ) = x )
	isgrpix.6	|- ( x e. B -> N e. B )
	isgrpix.7	|- ( x e. B -> ( N .+ x ) = .0. )
Assertion	isgrpix	|- G e. Grp

Proof

Step	Hyp	Ref	Expression
1		isgrpix.a	|- B e. _V
2		isgrpix.b	|- .+ e. _V
3		isgrpix.g	|- G = { <. 1 , B >. , <. 2 , .+ >. }
4		isgrpix.2	|- ( ( x e. B /\ y e. B ) -> ( x .+ y ) e. B )
5		isgrpix.3	|- ( ( x e. B /\ y e. B /\ z e. B ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
6		isgrpix.z	|- .0. e. B
7		isgrpix.5	|- ( x e. B -> ( .0. .+ x ) = x )
8		isgrpix.6	|- ( x e. B -> N e. B )
9		isgrpix.7	|- ( x e. B -> ( N .+ x ) = .0. )
10	1 2 3	grpbasex	|- B = ( Base ` G )
11	1 2 3	grpplusgx	|- .+ = ( +g ` G )
12	10 11 4 5 6 7 8 9	isgrpi	|- G e. Grp