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 
|- X e. _V
isgrpoi.2 
|- G : ( X X. X ) --> X
isgrpoi.3 
|- ( ( x e. X /\ y e. X /\ z e. X ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) )
isgrpoi.4 
|- U e. X
isgrpoi.5 
|- ( x e. X -> ( U G x ) = x )
isgrpoi.6 
|- ( x e. X -> N e. X )
isgrpoi.7 
|- ( x e. X -> ( N G x ) = U )
Assertion isgrpoi 
|- G e. GrpOp

Proof

Step Hyp Ref Expression
1 isgrpoi.1 
 |-  X e. _V
2 isgrpoi.2 
 |-  G : ( X X. X ) --> X
3 isgrpoi.3 
 |-  ( ( x e. X /\ y e. X /\ z e. X ) -> ( ( x G y ) G z ) = ( x G ( y G z ) ) )
4 isgrpoi.4 
 |-  U e. X
5 isgrpoi.5 
 |-  ( x e. X -> ( U G x ) = x )
6 isgrpoi.6 
 |-  ( x e. X -> N e. X )
7 isgrpoi.7 
 |-  ( x e. X -> ( N G x ) = U )
8 3 rgen3 
 |-  A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) )
9 oveq1 
 |-  ( y = N -> ( y G x ) = ( N G x ) )
10 9 eqeq1d 
 |-  ( y = N -> ( ( y G x ) = U <-> ( N G x ) = U ) )
11 10 rspcev 
 |-  ( ( N e. X /\ ( N G x ) = U ) -> E. y e. X ( y G x ) = U )
12 6 7 11 syl2anc 
 |-  ( x e. X -> E. y e. X ( y G x ) = U )
13 5 12 jca 
 |-  ( x e. X -> ( ( U G x ) = x /\ E. y e. X ( y G x ) = U ) )
14 13 rgen 
 |-  A. x e. X ( ( U G x ) = x /\ E. y e. X ( y G x ) = U )
15 oveq1 
 |-  ( u = U -> ( u G x ) = ( U G x ) )
16 15 eqeq1d 
 |-  ( u = U -> ( ( u G x ) = x <-> ( U G x ) = x ) )
17 eqeq2 
 |-  ( u = U -> ( ( y G x ) = u <-> ( y G x ) = U ) )
18 17 rexbidv 
 |-  ( u = U -> ( E. y e. X ( y G x ) = u <-> E. y e. X ( y G x ) = U ) )
19 16 18 anbi12d 
 |-  ( u = U -> ( ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) <-> ( ( U G x ) = x /\ E. y e. X ( y G x ) = U ) ) )
20 19 ralbidv 
 |-  ( u = U -> ( A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) <-> A. x e. X ( ( U G x ) = x /\ E. y e. X ( y G x ) = U ) ) )
21 20 rspcev 
 |-  ( ( U e. X /\ A. x e. X ( ( U G x ) = x /\ E. y e. X ( y G x ) = U ) ) -> E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) )
22 4 14 21 mp2an 
 |-  E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u )
23 1 1 xpex 
 |-  ( X X. X ) e. _V
24 fex 
 |-  ( ( G : ( X X. X ) --> X /\ ( X X. X ) e. _V ) -> G e. _V )
25 2 23 24 mp2an 
 |-  G e. _V
26 5 eqcomd 
 |-  ( x e. X -> x = ( U G x ) )
27 rspceov 
 |-  ( ( U e. X /\ x e. X /\ x = ( U G x ) ) -> E. y e. X E. z e. X x = ( y G z ) )
28 4 27 mp3an1 
 |-  ( ( x e. X /\ x = ( U G x ) ) -> E. y e. X E. z e. X x = ( y G z ) )
29 26 28 mpdan 
 |-  ( x e. X -> E. y e. X E. z e. X x = ( y G z ) )
30 29 rgen 
 |-  A. x e. X E. y e. X E. z e. X x = ( y G z )
31 foov 
 |-  ( G : ( X X. X ) -onto-> X <-> ( G : ( X X. X ) --> X /\ A. x e. X E. y e. X E. z e. X x = ( y G z ) ) )
32 2 30 31 mpbir2an 
 |-  G : ( X X. X ) -onto-> X
33 forn 
 |-  ( G : ( X X. X ) -onto-> X -> ran G = X )
34 32 33 ax-mp 
 |-  ran G = X
35 34 eqcomi 
 |-  X = ran G
36 35 isgrpo 
 |-  ( G e. _V -> ( G e. GrpOp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) ) ) )
37 25 36 ax-mp 
 |-  ( G e. GrpOp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) ) )
38 2 8 22 37 mpbir3an 
 |-  G e. GrpOp