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 ) ) ) )