Metamath Proof Explorer


Theorem isgrpoi

Description: Properties that determine a group operation. Read N as N ( x ) . (Contributed by NM, 4-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses isgrpoi.1 XV
isgrpoi.2 G:X×XX
isgrpoi.3 xXyXzXxGyGz=xGyGz
isgrpoi.4 UX
isgrpoi.5 xXUGx=x
isgrpoi.6 xXNX
isgrpoi.7 xXNGx=U
Assertion isgrpoi GGrpOp

Proof

Step Hyp Ref Expression
1 isgrpoi.1 XV
2 isgrpoi.2 G:X×XX
3 isgrpoi.3 xXyXzXxGyGz=xGyGz
4 isgrpoi.4 UX
5 isgrpoi.5 xXUGx=x
6 isgrpoi.6 xXNX
7 isgrpoi.7 xXNGx=U
8 3 rgen3 xXyXzXxGyGz=xGyGz
9 oveq1 y=NyGx=NGx
10 9 eqeq1d y=NyGx=UNGx=U
11 10 rspcev NXNGx=UyXyGx=U
12 6 7 11 syl2anc xXyXyGx=U
13 5 12 jca xXUGx=xyXyGx=U
14 13 rgen xXUGx=xyXyGx=U
15 oveq1 u=UuGx=UGx
16 15 eqeq1d u=UuGx=xUGx=x
17 eqeq2 u=UyGx=uyGx=U
18 17 rexbidv u=UyXyGx=uyXyGx=U
19 16 18 anbi12d u=UuGx=xyXyGx=uUGx=xyXyGx=U
20 19 ralbidv u=UxXuGx=xyXyGx=uxXUGx=xyXyGx=U
21 20 rspcev UXxXUGx=xyXyGx=UuXxXuGx=xyXyGx=u
22 4 14 21 mp2an uXxXuGx=xyXyGx=u
23 1 1 xpex X×XV
24 fex G:X×XXX×XVGV
25 2 23 24 mp2an GV
26 5 eqcomd xXx=UGx
27 rspceov UXxXx=UGxyXzXx=yGz
28 4 27 mp3an1 xXx=UGxyXzXx=yGz
29 26 28 mpdan xXyXzXx=yGz
30 29 rgen xXyXzXx=yGz
31 foov G:X×XontoXG:X×XXxXyXzXx=yGz
32 2 30 31 mpbir2an G:X×XontoX
33 forn G:X×XontoXranG=X
34 32 33 ax-mp ranG=X
35 34 eqcomi X=ranG
36 35 isgrpo GVGGrpOpG:X×XXxXyXzXxGyGz=xGyGzuXxXuGx=xyXyGx=u
37 25 36 ax-mp GGrpOpG:X×XXxXyXzXxGyGz=xGyGzuXxXuGx=xyXyGx=u
38 2 8 22 37 mpbir3an GGrpOp