Metamath Proof Explorer


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 V
isgrpix.b + ˙ V
isgrpix.g G = 1 B 2 + ˙
isgrpix.2 x B y B x + ˙ y B
isgrpix.3 x B y B z B x + ˙ y + ˙ z = x + ˙ y + ˙ z
isgrpix.z 0 ˙ B
isgrpix.5 x B 0 ˙ + ˙ x = x
isgrpix.6 x B N B
isgrpix.7 x B N + ˙ x = 0 ˙
Assertion isgrpix G Grp

Proof

Step Hyp Ref Expression
1 isgrpix.a B V
2 isgrpix.b + ˙ V
3 isgrpix.g G = 1 B 2 + ˙
4 isgrpix.2 x B y B x + ˙ y B
5 isgrpix.3 x B y B z B x + ˙ y + ˙ z = x + ˙ y + ˙ z
6 isgrpix.z 0 ˙ B
7 isgrpix.5 x B 0 ˙ + ˙ x = x
8 isgrpix.6 x B N B
9 isgrpix.7 x B N + ˙ x = 0 ˙
10 1 2 3 grpbasex B = Base G
11 1 2 3 grpplusgx + ˙ = + G
12 10 11 4 5 6 7 8 9 isgrpi G Grp