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=ranG
Assertion isgrpo GAGGrpOpG:X×XXxXyXzXxGyGz=xGyGzuXxXuGx=xyXyGx=u

Proof

Step Hyp Ref Expression
1 isgrp.1 X=ranG
2 feq1 g=Gg:t×ttG:t×tt
3 oveq g=Gxgygz=xgyGz
4 oveq g=Gxgy=xGy
5 4 oveq1d g=GxgyGz=xGyGz
6 3 5 eqtrd g=Gxgygz=xGyGz
7 oveq g=Gxgygz=xGygz
8 oveq g=Gygz=yGz
9 8 oveq2d g=GxGygz=xGyGz
10 7 9 eqtrd g=Gxgygz=xGyGz
11 6 10 eqeq12d g=Gxgygz=xgygzxGyGz=xGyGz
12 11 ralbidv g=Gztxgygz=xgygzztxGyGz=xGyGz
13 12 2ralbidv g=Gxtytztxgygz=xgygzxtytztxGyGz=xGyGz
14 oveq g=Gugx=uGx
15 14 eqeq1d g=Gugx=xuGx=x
16 oveq g=Gygx=yGx
17 16 eqeq1d g=Gygx=uyGx=u
18 17 rexbidv g=Gytygx=uytyGx=u
19 15 18 anbi12d g=Gugx=xytygx=uuGx=xytyGx=u
20 19 rexralbidv g=Gutxtugx=xytygx=uutxtuGx=xytyGx=u
21 2 13 20 3anbi123d g=Gg:t×ttxtytztxgygz=xgygzutxtugx=xytygx=uG:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=u
22 21 exbidv g=Gtg:t×ttxtytztxgygz=xgygzutxtugx=xytygx=utG:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=u
23 df-grpo GrpOp=g|tg:t×ttxtytztxgygz=xgygzutxtugx=xytygx=u
24 22 23 elab2g GAGGrpOptG:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=u
25 simpl uGx=xytyGx=uuGx=x
26 25 ralimi xtuGx=xytyGx=uxtuGx=x
27 oveq2 x=zuGx=uGz
28 id x=zx=z
29 27 28 eqeq12d x=zuGx=xuGz=z
30 eqcom uGz=zz=uGz
31 29 30 bitrdi x=zuGx=xz=uGz
32 31 rspcv ztxtuGx=xz=uGz
33 oveq2 y=zuGy=uGz
34 33 rspceeqv ztz=uGzytz=uGy
35 34 ex ztz=uGzytz=uGy
36 32 35 syld ztxtuGx=xytz=uGy
37 26 36 syl5 ztxtuGx=xytyGx=uytz=uGy
38 37 reximdv ztutxtuGx=xytyGx=uutytz=uGy
39 38 impcom utxtuGx=xytyGx=uztutytz=uGy
40 39 ralrimiva utxtuGx=xytyGx=uztutytz=uGy
41 40 anim2i G:t×ttutxtuGx=xytyGx=uG:t×ttztutytz=uGy
42 foov G:t×tontotG:t×ttztutytz=uGy
43 41 42 sylibr G:t×ttutxtuGx=xytyGx=uG:t×tontot
44 forn G:t×tontotranG=t
45 44 eqcomd G:t×tontott=ranG
46 43 45 syl G:t×ttutxtuGx=xytyGx=ut=ranG
47 46 3adant2 G:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=ut=ranG
48 47 pm4.71ri G:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=ut=ranGG:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=u
49 48 exbii tG:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=utt=ranGG:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=u
50 24 49 bitrdi GAGGrpOptt=ranGG:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=u
51 rnexg GAranGV
52 1 eqeq2i t=Xt=ranG
53 xpeq1 t=Xt×t=X×t
54 xpeq2 t=XX×t=X×X
55 53 54 eqtrd t=Xt×t=X×X
56 55 feq2d t=XG:t×ttG:X×Xt
57 feq3 t=XG:X×XtG:X×XX
58 56 57 bitrd t=XG:t×ttG:X×XX
59 raleq t=XztxGyGz=xGyGzzXxGyGz=xGyGz
60 59 raleqbi1dv t=XytztxGyGz=xGyGzyXzXxGyGz=xGyGz
61 60 raleqbi1dv t=XxtytztxGyGz=xGyGzxXyXzXxGyGz=xGyGz
62 rexeq t=XytyGx=uyXyGx=u
63 62 anbi2d t=XuGx=xytyGx=uuGx=xyXyGx=u
64 63 raleqbi1dv t=XxtuGx=xytyGx=uxXuGx=xyXyGx=u
65 64 rexeqbi1dv t=XutxtuGx=xytyGx=uuXxXuGx=xyXyGx=u
66 58 61 65 3anbi123d t=XG:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=uG:X×XXxXyXzXxGyGz=xGyGzuXxXuGx=xyXyGx=u
67 52 66 sylbir t=ranGG:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=uG:X×XXxXyXzXxGyGz=xGyGzuXxXuGx=xyXyGx=u
68 67 ceqsexgv ranGVtt=ranGG:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=uG:X×XXxXyXzXxGyGz=xGyGzuXxXuGx=xyXyGx=u
69 51 68 syl GAtt=ranGG:t×ttxtytztxGyGz=xGyGzutxtuGx=xytyGx=uG:X×XXxXyXzXxGyGz=xGyGzuXxXuGx=xyXyGx=u
70 50 69 bitrd GAGGrpOpG:X×XXxXyXzXxGyGz=xGyGzuXxXuGx=xyXyGx=u