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 A G GrpOp G : X × X X x X y X z X x G y G z = x G y G z u X x X u G x = x y X y G x = u

Proof

Step Hyp Ref Expression
1 isgrp.1 X = ran G
2 feq1 g = G g : t × t t G : t × 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 z t x g y g z = x g y g z z t x G y G z = x G y G z
13 12 2ralbidv g = G x t y t z t x g y g z = x g y g z x t y t z 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 y t y g x = u y t y G x = u
19 15 18 anbi12d g = G u g x = x y t y g x = u u G x = x y t y G x = u
20 19 rexralbidv g = G u t x t u g x = x y t y g x = u u t x t u G x = x y t y G x = u
21 2 13 20 3anbi123d g = G g : t × t t x t y t z t x g y g z = x g y g z u t x t u g x = x y t y g x = u G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u
22 21 exbidv g = G t g : t × t t x t y t z t x g y g z = x g y g z u t x t u g x = x y t y g x = u t G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u
23 df-grpo GrpOp = g | t g : t × t t x t y t z t x g y g z = x g y g z u t x t u g x = x y t y g x = u
24 22 23 elab2g G A G GrpOp t G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u
25 simpl u G x = x y t y G x = u u G x = x
26 25 ralimi x t u G x = x y t y G x = u x 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 t x t u G x = x z = u G z
33 oveq2 y = z u G y = u G z
34 33 rspceeqv z t z = u G z y t z = u G y
35 34 ex z t z = u G z y t z = u G y
36 32 35 syld z t x t u G x = x y t z = u G y
37 26 36 syl5 z t x t u G x = x y t y G x = u y t z = u G y
38 37 reximdv z t u t x t u G x = x y t y G x = u u t y t z = u G y
39 38 impcom u t x t u G x = x y t y G x = u z t u t y t z = u G y
40 39 ralrimiva u t x t u G x = x y t y G x = u z t u t y t z = u G y
41 40 anim2i G : t × t t u t x t u G x = x y t y G x = u G : t × t t z t u t y t z = u G y
42 foov G : t × t onto t G : t × t t z t u t y t z = u G y
43 41 42 sylibr G : t × t t u t x t u G x = x y t y G x = u G : t × t onto t
44 forn G : t × t onto t ran G = t
45 44 eqcomd G : t × t onto t t = ran G
46 43 45 syl G : t × t t u t x t u G x = x y t y G x = u t = ran G
47 46 3adant2 G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u t = ran G
48 47 pm4.71ri G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u t = ran G G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u
49 48 exbii t G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u t t = ran G G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u
50 24 49 bitrdi G A G GrpOp t t = ran G G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u
51 rnexg G A ran G V
52 1 eqeq2i t = X t = ran G
53 xpeq1 t = X t × t = X × t
54 xpeq2 t = X X × t = X × X
55 53 54 eqtrd t = X t × t = X × X
56 55 feq2d t = X G : t × t t G : X × X t
57 feq3 t = X G : X × X t G : X × X X
58 56 57 bitrd t = X G : t × t t G : X × X X
59 raleq t = X z t x G y G z = x G y G z z X x G y G z = x G y G z
60 59 raleqbi1dv t = X y t z t x G y G z = x G y G z y X z X x G y G z = x G y G z
61 60 raleqbi1dv t = X x t y t z t x G y G z = x G y G z x X y X z X x G y G z = x G y G z
62 rexeq t = X y t y G x = u y X y G x = u
63 62 anbi2d t = X u G x = x y t y G x = u u G x = x y X y G x = u
64 63 raleqbi1dv t = X x t u G x = x y t y G x = u x X u G x = x y X y G x = u
65 64 rexeqbi1dv t = X u t x t u G x = x y t y G x = u u X x X u G x = x y X y G x = u
66 58 61 65 3anbi123d t = X G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u G : X × X X x X y X z X x G y G z = x G y G z u X x X u G x = x y X y G x = u
67 52 66 sylbir t = ran G G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u G : X × X X x X y X z X x G y G z = x G y G z u X x X u G x = x y X y G x = u
68 67 ceqsexgv ran G V t t = ran G G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u G : X × X X x X y X z X x G y G z = x G y G z u X x X u G x = x y X y G x = u
69 51 68 syl G A t t = ran G G : t × t t x t y t z t x G y G z = x G y G z u t x t u G x = x y t y G x = u G : X × X X x X y X z X x G y G z = x G y G z u X x X u G x = x y X y G x = u
70 50 69 bitrd G A G GrpOp G : X × X X x X y X z X x G y G z = x G y G z u X x X u G x = x y X y G x = u