MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  isga Structured version   Unicode version

Theorem isga 16881
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 16896). 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.)
Hypotheses
Ref Expression
isga.1  |-  X  =  ( Base `  G
)
isga.2  |-  .+  =  ( +g  `  G )
isga.3  |-  .0.  =  ( 0g `  G )
Assertion
Ref Expression
isga  |-  (  .(+)  e.  ( G  GrpAct  Y )  <-> 
( ( G  e. 
Grp  /\  Y  e.  _V )  /\  (  .(+)  : ( X  X.  Y ) --> Y  /\  A. x  e.  Y  ( (  .0.  .(+)  x )  =  x  /\  A. y  e.  X  A. z  e.  X  (
( y  .+  z
)  .(+)  x )  =  ( y  .(+)  ( z 
.(+)  x ) ) ) ) ) )
Distinct variable groups:    x, y,
z, G    y, X, z    x, Y, y, z   
x,  .(+) , y, z
Allowed substitution hints:    .+ ( x, y, z)    X( x)    .0. ( x, y, z)

Proof of Theorem isga
Dummy variables  g 
b  m  s are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-ga 16880 . . 3  |-  GrpAct  =  ( g  e.  Grp , 
s  e.  _V  |->  [_ ( Base `  g )  /  b ]_ {
m  e.  ( s  ^m  ( b  X.  s ) )  | 
A. x  e.  s  ( ( ( 0g
`  g ) m x )  =  x  /\  A. y  e.  b  A. z  e.  b  ( ( y ( +g  `  g
) z ) m x )  =  ( y m ( z m x ) ) ) } )
21elmpt2cl 6462 . 2  |-  (  .(+)  e.  ( G  GrpAct  Y )  ->  ( G  e. 
Grp  /\  Y  e.  _V ) )
3 fvex 5828 . . . . . . . 8  |-  ( Base `  g )  e.  _V
43a1i 11 . . . . . . 7  |-  ( ( g  =  G  /\  s  =  Y )  ->  ( Base `  g
)  e.  _V )
5 simplr 760 . . . . . . . . 9  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  s  =  Y )
6 id 22 . . . . . . . . . . 11  |-  ( b  =  ( Base `  g
)  ->  b  =  ( Base `  g )
)
7 simpl 458 . . . . . . . . . . . . 13  |-  ( ( g  =  G  /\  s  =  Y )  ->  g  =  G )
87fveq2d 5822 . . . . . . . . . . . 12  |-  ( ( g  =  G  /\  s  =  Y )  ->  ( Base `  g
)  =  ( Base `  G ) )
9 isga.1 . . . . . . . . . . . 12  |-  X  =  ( Base `  G
)
108, 9syl6eqr 2474 . . . . . . . . . . 11  |-  ( ( g  =  G  /\  s  =  Y )  ->  ( Base `  g
)  =  X )
116, 10sylan9eqr 2478 . . . . . . . . . 10  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  b  =  X )
1211, 5xpeq12d 4814 . . . . . . . . 9  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  (
b  X.  s )  =  ( X  X.  Y ) )
135, 12oveq12d 6260 . . . . . . . 8  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  (
s  ^m  ( b  X.  s ) )  =  ( Y  ^m  ( X  X.  Y ) ) )
14 simpll 758 . . . . . . . . . . . . . 14  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  g  =  G )
1514fveq2d 5822 . . . . . . . . . . . . 13  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  ( 0g `  g )  =  ( 0g `  G
) )
16 isga.3 . . . . . . . . . . . . 13  |-  .0.  =  ( 0g `  G )
1715, 16syl6eqr 2474 . . . . . . . . . . . 12  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  ( 0g `  g )  =  .0.  )
1817oveq1d 6257 . . . . . . . . . . 11  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  (
( 0g `  g
) m x )  =  (  .0.  m x ) )
1918eqeq1d 2424 . . . . . . . . . 10  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  (
( ( 0g `  g ) m x )  =  x  <->  (  .0.  m x )  =  x ) )
2014fveq2d 5822 . . . . . . . . . . . . . . . 16  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  ( +g  `  g )  =  ( +g  `  G
) )
21 isga.2 . . . . . . . . . . . . . . . 16  |-  .+  =  ( +g  `  G )
2220, 21syl6eqr 2474 . . . . . . . . . . . . . . 15  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  ( +g  `  g )  = 
.+  )
2322oveqd 6259 . . . . . . . . . . . . . 14  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  (
y ( +g  `  g
) z )  =  ( y  .+  z
) )
2423oveq1d 6257 . . . . . . . . . . . . 13  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  (
( y ( +g  `  g ) z ) m x )  =  ( ( y  .+  z ) m x ) )
2524eqeq1d 2424 . . . . . . . . . . . 12  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  (
( ( y ( +g  `  g ) z ) m x )  =  ( y m ( z m x ) )  <->  ( (
y  .+  z )
m x )  =  ( y m ( z m x ) ) ) )
2611, 25raleqbidv 2972 . . . . . . . . . . 11  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  ( A. z  e.  b 
( ( y ( +g  `  g ) z ) m x )  =  ( y m ( z m x ) )  <->  A. z  e.  X  ( (
y  .+  z )
m x )  =  ( y m ( z m x ) ) ) )
2711, 26raleqbidv 2972 . . . . . . . . . 10  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  ( A. y  e.  b  A. z  e.  b 
( ( y ( +g  `  g ) z ) m x )  =  ( y m ( z m x ) )  <->  A. y  e.  X  A. z  e.  X  ( (
y  .+  z )
m x )  =  ( y m ( z m x ) ) ) )
2819, 27anbi12d 715 . . . . . . . . 9  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  (
( ( ( 0g
`  g ) m x )  =  x  /\  A. y  e.  b  A. z  e.  b  ( ( y ( +g  `  g
) z ) m x )  =  ( y m ( z m x ) ) )  <->  ( (  .0.  m x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( (
y  .+  z )
m x )  =  ( y m ( z m x ) ) ) ) )
295, 28raleqbidv 2972 . . . . . . . 8  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  ( A. x  e.  s 
( ( ( 0g
`  g ) m x )  =  x  /\  A. y  e.  b  A. z  e.  b  ( ( y ( +g  `  g
) z ) m x )  =  ( y m ( z m x ) ) )  <->  A. x  e.  Y  ( (  .0.  m x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( ( y 
.+  z ) m x )  =  ( y m ( z m x ) ) ) ) )
3013, 29rabeqbidv 3011 . . . . . . 7  |-  ( ( ( g  =  G  /\  s  =  Y )  /\  b  =  ( Base `  g
) )  ->  { m  e.  ( s  ^m  (
b  X.  s ) )  |  A. x  e.  s  ( (
( 0g `  g
) m x )  =  x  /\  A. y  e.  b  A. z  e.  b  (
( y ( +g  `  g ) z ) m x )  =  ( y m ( z m x ) ) ) }  =  { m  e.  ( Y  ^m  ( X  X.  Y ) )  | 
A. x  e.  Y  ( (  .0.  m x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( ( y 
.+  z ) m x )  =  ( y m ( z m x ) ) ) } )
314, 30csbied 3358 . . . . . 6  |-  ( ( g  =  G  /\  s  =  Y )  ->  [_ ( Base `  g
)  /  b ]_ { m  e.  (
s  ^m  ( b  X.  s ) )  | 
A. x  e.  s  ( ( ( 0g
`  g ) m x )  =  x  /\  A. y  e.  b  A. z  e.  b  ( ( y ( +g  `  g
) z ) m x )  =  ( y m ( z m x ) ) ) }  =  {
m  e.  ( Y  ^m  ( X  X.  Y ) )  | 
A. x  e.  Y  ( (  .0.  m x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( ( y 
.+  z ) m x )  =  ( y m ( z m x ) ) ) } )
32 ovex 6270 . . . . . . 7  |-  ( Y  ^m  ( X  X.  Y ) )  e. 
_V
3332rabex 4511 . . . . . 6  |-  { m  e.  ( Y  ^m  ( X  X.  Y ) )  |  A. x  e.  Y  ( (  .0.  m x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( (
y  .+  z )
m x )  =  ( y m ( z m x ) ) ) }  e.  _V
3431, 1, 33ovmpt2a 6378 . . . . 5  |-  ( ( G  e.  Grp  /\  Y  e.  _V )  ->  ( G  GrpAct  Y )  =  { m  e.  ( Y  ^m  ( X  X.  Y ) )  |  A. x  e.  Y  ( (  .0.  m x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( (
y  .+  z )
m x )  =  ( y m ( z m x ) ) ) } )
3534eleq2d 2485 . . . 4  |-  ( ( G  e.  Grp  /\  Y  e.  _V )  ->  (  .(+)  e.  ( G  GrpAct  Y )  <->  .(+)  e.  {
m  e.  ( Y  ^m  ( X  X.  Y ) )  | 
A. x  e.  Y  ( (  .0.  m x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( ( y 
.+  z ) m x )  =  ( y m ( z m x ) ) ) } ) )
36 oveq 6248 . . . . . . . 8  |-  ( m  =  .(+)  ->  (  .0.  m x )  =  (  .0.  .(+)  x ) )
3736eqeq1d 2424 . . . . . . 7  |-  ( m  =  .(+)  ->  ( (  .0.  m x )  =  x  <->  (  .0.  .(+) 
x )  =  x ) )
38 oveq 6248 . . . . . . . . 9  |-  ( m  =  .(+)  ->  ( ( y  .+  z ) m x )  =  ( ( y  .+  z )  .(+)  x ) )
39 oveq 6248 . . . . . . . . . 10  |-  ( m  =  .(+)  ->  ( y m ( z m x ) )  =  ( y  .(+)  ( z m x ) ) )
40 oveq 6248 . . . . . . . . . . 11  |-  ( m  =  .(+)  ->  ( z m x )  =  ( z  .(+)  x ) )
4140oveq2d 6258 . . . . . . . . . 10  |-  ( m  =  .(+)  ->  ( y 
.(+)  ( z m x ) )  =  ( y  .(+)  ( z 
.(+)  x ) ) )
4239, 41eqtrd 2456 . . . . . . . . 9  |-  ( m  =  .(+)  ->  ( y m ( z m x ) )  =  ( y  .(+)  ( z 
.(+)  x ) ) )
4338, 42eqeq12d 2437 . . . . . . . 8  |-  ( m  =  .(+)  ->  ( ( ( y  .+  z
) m x )  =  ( y m ( z m x ) )  <->  ( (
y  .+  z )  .(+)  x )  =  ( y  .(+)  ( z  .(+)  x ) ) ) )
44432ralbidv 2803 . . . . . . 7  |-  ( m  =  .(+)  ->  ( A. y  e.  X  A. z  e.  X  (
( y  .+  z
) m x )  =  ( y m ( z m x ) )  <->  A. y  e.  X  A. z  e.  X  ( (
y  .+  z )  .(+)  x )  =  ( y  .(+)  ( z  .(+)  x ) ) ) )
4537, 44anbi12d 715 . . . . . 6  |-  ( m  =  .(+)  ->  ( ( (  .0.  m x )  =  x  /\  A. y  e.  X  A. z  e.  X  (
( y  .+  z
) m x )  =  ( y m ( z m x ) ) )  <->  ( (  .0.  .(+)  x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( (
y  .+  z )  .(+)  x )  =  ( y  .(+)  ( z  .(+)  x ) ) ) ) )
4645ralbidv 2798 . . . . 5  |-  ( m  =  .(+)  ->  ( A. x  e.  Y  (
(  .0.  m x )  =  x  /\  A. y  e.  X  A. z  e.  X  (
( y  .+  z
) m x )  =  ( y m ( z m x ) ) )  <->  A. x  e.  Y  ( (  .0.  .(+)  x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( (
y  .+  z )  .(+)  x )  =  ( y  .(+)  ( z  .(+)  x ) ) ) ) )
4746elrab 3164 . . . 4  |-  (  .(+)  e. 
{ m  e.  ( Y  ^m  ( X  X.  Y ) )  |  A. x  e.  Y  ( (  .0.  m x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( (
y  .+  z )
m x )  =  ( y m ( z m x ) ) ) }  <->  (  .(+)  e.  ( Y  ^m  ( X  X.  Y ) )  /\  A. x  e.  Y  ( (  .0.  .(+)  x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( ( y 
.+  z )  .(+)  x )  =  ( y 
.(+)  ( z  .(+)  x ) ) ) ) )
4835, 47syl6bb 264 . . 3  |-  ( ( G  e.  Grp  /\  Y  e.  _V )  ->  (  .(+)  e.  ( G  GrpAct  Y )  <->  (  .(+)  e.  ( Y  ^m  ( X  X.  Y ) )  /\  A. x  e.  Y  ( (  .0.  .(+)  x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( ( y 
.+  z )  .(+)  x )  =  ( y 
.(+)  ( z  .(+)  x ) ) ) ) ) )
49 simpr 462 . . . . 5  |-  ( ( G  e.  Grp  /\  Y  e.  _V )  ->  Y  e.  _V )
50 fvex 5828 . . . . . . 7  |-  ( Base `  G )  e.  _V
519, 50eqeltri 2496 . . . . . 6  |-  X  e. 
_V
52 xpexg 6544 . . . . . 6  |-  ( ( X  e.  _V  /\  Y  e.  _V )  ->  ( X  X.  Y
)  e.  _V )
5351, 49, 52sylancr 667 . . . . 5  |-  ( ( G  e.  Grp  /\  Y  e.  _V )  ->  ( X  X.  Y
)  e.  _V )
5449, 53elmapd 7434 . . . 4  |-  ( ( G  e.  Grp  /\  Y  e.  _V )  ->  (  .(+)  e.  ( Y  ^m  ( X  X.  Y ) )  <->  .(+)  : ( X  X.  Y ) --> Y ) )
5554anbi1d 709 . . 3  |-  ( ( G  e.  Grp  /\  Y  e.  _V )  ->  ( (  .(+)  e.  ( Y  ^m  ( X  X.  Y ) )  /\  A. x  e.  Y  ( (  .0.  .(+)  x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( ( y 
.+  z )  .(+)  x )  =  ( y 
.(+)  ( z  .(+)  x ) ) ) )  <-> 
(  .(+)  : ( X  X.  Y ) --> Y  /\  A. x  e.  Y  ( (  .0.  .(+)  x )  =  x  /\  A. y  e.  X  A. z  e.  X  ( ( y 
.+  z )  .(+)  x )  =  ( y 
.(+)  ( z  .(+)  x ) ) ) ) ) )
5648, 55bitrd 256 . 2  |-  ( ( G  e.  Grp  /\  Y  e.  _V )  ->  (  .(+)  e.  ( G  GrpAct  Y )  <->  (  .(+)  : ( X  X.  Y
) --> Y  /\  A. x  e.  Y  (
(  .0.  .(+)  x )  =  x  /\  A. y  e.  X  A. z  e.  X  (
( y  .+  z
)  .(+)  x )  =  ( y  .(+)  ( z 
.(+)  x ) ) ) ) ) )
572, 56biadan2 646 1  |-  (  .(+)  e.  ( G  GrpAct  Y )  <-> 
( ( G  e. 
Grp  /\  Y  e.  _V )  /\  (  .(+)  : ( X  X.  Y ) --> Y  /\  A. x  e.  Y  ( (  .0.  .(+)  x )  =  x  /\  A. y  e.  X  A. z  e.  X  (
( y  .+  z
)  .(+)  x )  =  ( y  .(+)  ( z 
.(+)  x ) ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370    = wceq 1437    e. wcel 1872   A.wral 2708   {crab 2712   _Vcvv 3016   [_csb 3331    X. cxp 4787   -->wf 5533   ` cfv 5537  (class class class)co 6242    ^m cmap 7420   Basecbs 15057   +g cplusg 15126   0gc0g 15274   Grpcgrp 16605    GrpAct cga 16879
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402  ax-sep 4482  ax-nul 4491  ax-pow 4538  ax-pr 4596  ax-un 6534
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2274  df-mo 2275  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2552  df-ne 2595  df-ral 2713  df-rex 2714  df-rab 2717  df-v 3018  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3698  df-if 3848  df-pw 3919  df-sn 3935  df-pr 3937  df-op 3941  df-uni 4156  df-br 4360  df-opab 4419  df-id 4704  df-xp 4795  df-rel 4796  df-cnv 4797  df-co 4798  df-dm 4799  df-rn 4800  df-iota 5501  df-fun 5539  df-fn 5540  df-f 5541  df-fv 5545  df-ov 6245  df-oprab 6246  df-mpt2 6247  df-map 7422  df-ga 16880
This theorem is referenced by:  gagrp  16882  gaset  16883  gagrpid  16884  gaf  16885  gaass  16887  ga0  16888  gaid  16889  subgga  16890  gass  16891  gasubg  16892  lactghmga  16981  sylow1lem2  17187  sylow2blem2  17209  sylow3lem1  17215
  Copyright terms: Public domain W3C validator