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=BaseG
isgrpi.p +˙=+G
isgrpi.c xByBx+˙yB
isgrpi.a xByBzBx+˙y+˙z=x+˙y+˙z
isgrpi.z 0˙B
isgrpi.i xB0˙+˙x=x
isgrpi.n xBNB
isgrpi.j xBN+˙x=0˙
Assertion isgrpi GGrp

Proof

Step Hyp Ref Expression
1 isgrpi.b B=BaseG
2 isgrpi.p +˙=+G
3 isgrpi.c xByBx+˙yB
4 isgrpi.a xByBzBx+˙y+˙z=x+˙y+˙z
5 isgrpi.z 0˙B
6 isgrpi.i xB0˙+˙x=x
7 isgrpi.n xBNB
8 isgrpi.j xBN+˙x=0˙
9 1 a1i B=BaseG
10 2 a1i +˙=+G
11 3 3adant1 xByBx+˙yB
12 4 adantl xByBzBx+˙y+˙z=x+˙y+˙z
13 5 a1i 0˙B
14 6 adantl xB0˙+˙x=x
15 7 adantl xBNB
16 8 adantl xBN+˙x=0˙
17 9 10 11 12 13 14 15 16 isgrpd GGrp
18 17 mptru GGrp