Metamath Proof Explorer

Theorem isgrpo

Description: The predicate "is a group operation." Note that X is the base set of the group. (Contributed by NM, 10-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypothesis isgrp.1 
|- X = ran G
Assertion isgrpo 
|- ( G e. A -> ( 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 isgrp.1 
 |-  X = ran G
2 feq1 
 |-  ( g = G -> ( g : ( t X. t ) --> t <-> G : ( t X. t ) --> t ) )
3 oveq 
 |-  ( g = G -> ( ( x g y ) g z ) = ( ( x g y ) G z ) )
4 oveq 
 |-  ( g = G -> ( x g y ) = ( x G y ) )
5 4 oveq1d 
 |-  ( g = G -> ( ( x g y ) G z ) = ( ( x G y ) G z ) )
6 3 5 eqtrd 
 |-  ( g = G -> ( ( x g y ) g z ) = ( ( x G y ) G z ) )
7 oveq 
 |-  ( g = G -> ( x g ( y g z ) ) = ( x G ( y g z ) ) )
8 oveq 
 |-  ( g = G -> ( y g z ) = ( y G z ) )
9 8 oveq2d 
 |-  ( g = G -> ( x G ( y g z ) ) = ( x G ( y G z ) ) )
10 7 9 eqtrd 
 |-  ( g = G -> ( x g ( y g z ) ) = ( x G ( y G z ) ) )
11 6 10 eqeq12d 
 |-  ( g = G -> ( ( ( x g y ) g z ) = ( x g ( y g z ) ) <-> ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
12 11 ralbidv 
 |-  ( g = G -> ( A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) ) <-> A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
13 12 2ralbidv 
 |-  ( g = G -> ( A. x e. t A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) ) <-> A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
14 oveq 
 |-  ( g = G -> ( u g x ) = ( u G x ) )
15 14 eqeq1d 
 |-  ( g = G -> ( ( u g x ) = x <-> ( u G x ) = x ) )
16 oveq 
 |-  ( g = G -> ( y g x ) = ( y G x ) )
17 16 eqeq1d 
 |-  ( g = G -> ( ( y g x ) = u <-> ( y G x ) = u ) )
18 17 rexbidv 
 |-  ( g = G -> ( E. y e. t ( y g x ) = u <-> E. y e. t ( y G x ) = u ) )
19 15 18 anbi12d 
 |-  ( g = G -> ( ( ( u g x ) = x /\ E. y e. t ( y g x ) = u ) <-> ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) )
20 19 rexralbidv 
 |-  ( g = G -> ( E. u e. t A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u ) <-> E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) )
21 2 13 20 3anbi123d 
 |-  ( g = G -> ( ( g : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) ) /\ E. u e. t A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u ) ) <-> ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) ) )
22 21 exbidv 
 |-  ( g = G -> ( E. t ( g : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) ) /\ E. u e. t A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u ) ) <-> E. t ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) ) )
23 df-grpo 
 |-  GrpOp = { g | E. t ( g : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x g y ) g z ) = ( x g ( y g z ) ) /\ E. u e. t A. x e. t ( ( u g x ) = x /\ E. y e. t ( y g x ) = u ) ) }
24 22 23 elab2g 
 |-  ( G e. A -> ( G e. GrpOp <-> E. t ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) ) )
25 simpl 
 |-  ( ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) -> ( u G x ) = x )
26 25 ralimi 
 |-  ( A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) -> A. x e. t ( u G x ) = x )
27 oveq2 
 |-  ( x = z -> ( u G x ) = ( u G z ) )
28 id 
 |-  ( x = z -> x = z )
29 27 28 eqeq12d 
 |-  ( x = z -> ( ( u G x ) = x <-> ( u G z ) = z ) )
30 eqcom 
 |-  ( ( u G z ) = z <-> z = ( u G z ) )
31 29 30 bitrdi 
 |-  ( x = z -> ( ( u G x ) = x <-> z = ( u G z ) ) )
32 31 rspcv 
 |-  ( z e. t -> ( A. x e. t ( u G x ) = x -> z = ( u G z ) ) )
33 oveq2 
 |-  ( y = z -> ( u G y ) = ( u G z ) )
34 33 rspceeqv 
 |-  ( ( z e. t /\ z = ( u G z ) ) -> E. y e. t z = ( u G y ) )
35 34 ex 
 |-  ( z e. t -> ( z = ( u G z ) -> E. y e. t z = ( u G y ) ) )
36 32 35 syld 
 |-  ( z e. t -> ( A. x e. t ( u G x ) = x -> E. y e. t z = ( u G y ) ) )
37 26 36 syl5 
 |-  ( z e. t -> ( A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) -> E. y e. t z = ( u G y ) ) )
38 37 reximdv 
 |-  ( z e. t -> ( E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) -> E. u e. t E. y e. t z = ( u G y ) ) )
39 38 impcom 
 |-  ( ( E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) /\ z e. t ) -> E. u e. t E. y e. t z = ( u G y ) )
40 39 ralrimiva 
 |-  ( E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) -> A. z e. t E. u e. t E. y e. t z = ( u G y ) )
41 40 anim2i 
 |-  ( ( G : ( t X. t ) --> t /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) -> ( G : ( t X. t ) --> t /\ A. z e. t E. u e. t E. y e. t z = ( u G y ) ) )
42 foov 
 |-  ( G : ( t X. t ) -onto-> t <-> ( G : ( t X. t ) --> t /\ A. z e. t E. u e. t E. y e. t z = ( u G y ) ) )
43 41 42 sylibr 
 |-  ( ( G : ( t X. t ) --> t /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) -> G : ( t X. t ) -onto-> t )
44 forn 
 |-  ( G : ( t X. t ) -onto-> t -> ran G = t )
45 44 eqcomd 
 |-  ( G : ( t X. t ) -onto-> t -> t = ran G )
46 43 45 syl 
 |-  ( ( G : ( t X. t ) --> t /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) -> t = ran G )
47 46 3adant2 
 |-  ( ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) -> t = ran G )
48 47 pm4.71ri 
 |-  ( ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) <-> ( t = ran G /\ ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) ) )
49 48 exbii 
 |-  ( E. t ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) <-> E. t ( t = ran G /\ ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) ) )
50 24 49 bitrdi 
 |-  ( G e. A -> ( G e. GrpOp <-> E. t ( t = ran G /\ ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) ) ) )
51 rnexg 
 |-  ( G e. A -> ran G e. _V )
52 1 eqeq2i 
 |-  ( t = X <-> t = ran G )
53 xpeq1 
 |-  ( t = X -> ( t X. t ) = ( X X. t ) )
54 xpeq2 
 |-  ( t = X -> ( X X. t ) = ( X X. X ) )
55 53 54 eqtrd 
 |-  ( t = X -> ( t X. t ) = ( X X. X ) )
56 55 feq2d 
 |-  ( t = X -> ( G : ( t X. t ) --> t <-> G : ( X X. X ) --> t ) )
57 feq3 
 |-  ( t = X -> ( G : ( X X. X ) --> t <-> G : ( X X. X ) --> X ) )
58 56 57 bitrd 
 |-  ( t = X -> ( G : ( t X. t ) --> t <-> G : ( X X. X ) --> X ) )
59 raleq 
 |-  ( t = X -> ( A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) <-> A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
60 59 raleqbi1dv 
 |-  ( t = X -> ( A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) <-> A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
61 60 raleqbi1dv 
 |-  ( t = X -> ( A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) <-> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) ) )
62 rexeq 
 |-  ( t = X -> ( E. y e. t ( y G x ) = u <-> E. y e. X ( y G x ) = u ) )
63 62 anbi2d 
 |-  ( t = X -> ( ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) <-> ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) ) )
64 63 raleqbi1dv 
 |-  ( t = X -> ( A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) <-> A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) ) )
65 64 rexeqbi1dv 
 |-  ( t = X -> ( E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) <-> E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) ) )
66 58 61 65 3anbi123d 
 |-  ( t = X -> ( ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) <-> ( 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 ) ) ) )
67 52 66 sylbir 
 |-  ( t = ran G -> ( ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) <-> ( 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 ) ) ) )
68 67 ceqsexgv 
 |-  ( ran G e. _V -> ( E. t ( t = ran G /\ ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) ) <-> ( 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 ) ) ) )
69 51 68 syl 
 |-  ( G e. A -> ( E. t ( t = ran G /\ ( G : ( t X. t ) --> t /\ A. x e. t A. y e. t A. z e. t ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. t A. x e. t ( ( u G x ) = x /\ E. y e. t ( y G x ) = u ) ) ) <-> ( 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 ) ) ) )
70 50 69 bitrd 
 |-  ( G e. A -> ( 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 ) ) ) )