Metamath Proof Explorer


Theorem isga

Description: The predicate "is a (left) group action". The group G is said to act on the base set Y of the action, which is not assumed to have any special properties. There is a related notion of right group action, but as the Wikipedia article explains, it is not mathematically interesting. The way actions are usually thought of is that each element g of G is a permutation of the elements of Y (see gapm ). Since group theory was classically about symmetry groups, it is therefore likely that the notion of group action was useful even in early group theory. (Contributed by Jeff Hankins, 10-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses isga.1 X=BaseG
isga.2 +˙=+G
isga.3 0˙=0G
Assertion isga ˙GGrpActYGGrpYV˙:X×YYxY0˙˙x=xyXzXy+˙z˙x=y˙z˙x

Proof

Step Hyp Ref Expression
1 isga.1 X=BaseG
2 isga.2 +˙=+G
3 isga.3 0˙=0G
4 df-ga GrpAct=gGrp,sVBaseg/bmsb×s|xs0gmx=xybzby+gzmx=ymzmx
5 4 elmpocl ˙GGrpActYGGrpYV
6 fvexd g=Gs=YBasegV
7 simplr g=Gs=Yb=Basegs=Y
8 id b=Basegb=Baseg
9 simpl g=Gs=Yg=G
10 9 fveq2d g=Gs=YBaseg=BaseG
11 10 1 eqtr4di g=Gs=YBaseg=X
12 8 11 sylan9eqr g=Gs=Yb=Basegb=X
13 12 7 xpeq12d g=Gs=Yb=Basegb×s=X×Y
14 7 13 oveq12d g=Gs=Yb=Basegsb×s=YX×Y
15 simpll g=Gs=Yb=Basegg=G
16 15 fveq2d g=Gs=Yb=Baseg0g=0G
17 16 3 eqtr4di g=Gs=Yb=Baseg0g=0˙
18 17 oveq1d g=Gs=Yb=Baseg0gmx=0˙mx
19 18 eqeq1d g=Gs=Yb=Baseg0gmx=x0˙mx=x
20 15 fveq2d g=Gs=Yb=Baseg+g=+G
21 20 2 eqtr4di g=Gs=Yb=Baseg+g=+˙
22 21 oveqd g=Gs=Yb=Basegy+gz=y+˙z
23 22 oveq1d g=Gs=Yb=Basegy+gzmx=y+˙zmx
24 23 eqeq1d g=Gs=Yb=Basegy+gzmx=ymzmxy+˙zmx=ymzmx
25 12 24 raleqbidv g=Gs=Yb=Basegzby+gzmx=ymzmxzXy+˙zmx=ymzmx
26 12 25 raleqbidv g=Gs=Yb=Basegybzby+gzmx=ymzmxyXzXy+˙zmx=ymzmx
27 19 26 anbi12d g=Gs=Yb=Baseg0gmx=xybzby+gzmx=ymzmx0˙mx=xyXzXy+˙zmx=ymzmx
28 7 27 raleqbidv g=Gs=Yb=Basegxs0gmx=xybzby+gzmx=ymzmxxY0˙mx=xyXzXy+˙zmx=ymzmx
29 14 28 rabeqbidv g=Gs=Yb=Basegmsb×s|xs0gmx=xybzby+gzmx=ymzmx=mYX×Y|xY0˙mx=xyXzXy+˙zmx=ymzmx
30 6 29 csbied g=Gs=YBaseg/bmsb×s|xs0gmx=xybzby+gzmx=ymzmx=mYX×Y|xY0˙mx=xyXzXy+˙zmx=ymzmx
31 ovex YX×YV
32 31 rabex mYX×Y|xY0˙mx=xyXzXy+˙zmx=ymzmxV
33 30 4 32 ovmpoa GGrpYVGGrpActY=mYX×Y|xY0˙mx=xyXzXy+˙zmx=ymzmx
34 33 eleq2d GGrpYV˙GGrpActY˙mYX×Y|xY0˙mx=xyXzXy+˙zmx=ymzmx
35 oveq m=˙0˙mx=0˙˙x
36 35 eqeq1d m=˙0˙mx=x0˙˙x=x
37 oveq m=˙y+˙zmx=y+˙z˙x
38 oveq m=˙ymzmx=y˙zmx
39 oveq m=˙zmx=z˙x
40 39 oveq2d m=˙y˙zmx=y˙z˙x
41 38 40 eqtrd m=˙ymzmx=y˙z˙x
42 37 41 eqeq12d m=˙y+˙zmx=ymzmxy+˙z˙x=y˙z˙x
43 42 2ralbidv m=˙yXzXy+˙zmx=ymzmxyXzXy+˙z˙x=y˙z˙x
44 36 43 anbi12d m=˙0˙mx=xyXzXy+˙zmx=ymzmx0˙˙x=xyXzXy+˙z˙x=y˙z˙x
45 44 ralbidv m=˙xY0˙mx=xyXzXy+˙zmx=ymzmxxY0˙˙x=xyXzXy+˙z˙x=y˙z˙x
46 45 elrab ˙mYX×Y|xY0˙mx=xyXzXy+˙zmx=ymzmx˙YX×YxY0˙˙x=xyXzXy+˙z˙x=y˙z˙x
47 34 46 bitrdi GGrpYV˙GGrpActY˙YX×YxY0˙˙x=xyXzXy+˙z˙x=y˙z˙x
48 simpr GGrpYVYV
49 1 fvexi XV
50 xpexg XVYVX×YV
51 49 48 50 sylancr GGrpYVX×YV
52 48 51 elmapd GGrpYV˙YX×Y˙:X×YY
53 52 anbi1d GGrpYV˙YX×YxY0˙˙x=xyXzXy+˙z˙x=y˙z˙x˙:X×YYxY0˙˙x=xyXzXy+˙z˙x=y˙z˙x
54 47 53 bitrd GGrpYV˙GGrpActY˙:X×YYxY0˙˙x=xyXzXy+˙z˙x=y˙z˙x
55 5 54 biadanii ˙GGrpActYGGrpYV˙:X×YYxY0˙˙x=xyXzXy+˙z˙x=y˙z˙x