# 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 syl6bb
` |-  ( 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 )`
` |-  ( ( 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 syl6bb
` |-  ( 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 ) ) ) )`