This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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