This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( Base ` G )
isga.2 
|- .+ = ( +g ` G )
isga.3 
|- .0. = ( 0g ` G )
Assertion 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isga.1 
 |-  X = ( Base ` G )
2 isga.2 
 |-  .+ = ( +g ` G )
3 isga.3 
 |-  .0. = ( 0g ` G )
4 df-ga 
 |-  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 ) ) ) } )
5 4 elmpocl 
 |-  ( .(+) e. ( G GrpAct Y ) -> ( G e. Grp /\ Y e. _V ) )
6 fvexd 
 |-  ( ( g = G /\ s = Y ) -> ( Base ` g ) e. _V )
7 simplr 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> s = Y )
8 id 
 |-  ( b = ( Base ` g ) -> b = ( Base ` g ) )
9 simpl 
 |-  ( ( g = G /\ s = Y ) -> g = G )
10 9 fveq2d 
 |-  ( ( g = G /\ s = Y ) -> ( Base ` g ) = ( Base ` G ) )
11 10 1 eqtr4di 
 |-  ( ( g = G /\ s = Y ) -> ( Base ` g ) = X )
12 8 11 sylan9eqr 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> b = X )
13 12 7 xpeq12d 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> ( b X. s ) = ( X X. Y ) )
14 7 13 oveq12d 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> ( s ^m ( b X. s ) ) = ( Y ^m ( X X. Y ) ) )
15 simpll 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> g = G )
16 15 fveq2d 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> ( 0g ` g ) = ( 0g ` G ) )
17 16 3 eqtr4di 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> ( 0g ` g ) = .0. )
18 17 oveq1d 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> ( ( 0g ` g ) m x ) = ( .0. m x ) )
19 18 eqeq1d 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> ( ( ( 0g ` g ) m x ) = x <-> ( .0. m x ) = x ) )
20 15 fveq2d 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> ( +g ` g ) = ( +g ` G ) )
21 20 2 eqtr4di 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> ( +g ` g ) = .+ )
22 21 oveqd 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> ( y ( +g ` g ) z ) = ( y .+ z ) )
23 22 oveq1d 
 |-  ( ( ( g = G /\ s = Y ) /\ b = ( Base ` g ) ) -> ( ( y ( +g ` g ) z ) m x ) = ( ( y .+ z ) m x ) )
24 23 eqeq1d 
 |-  ( ( ( 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 ) ) ) )
25 12 24 raleqbidv 
 |-  ( ( ( 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 ) ) ) )
26 12 25 raleqbidv 
 |-  ( ( ( 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 ) ) ) )
27 19 26 anbi12d 
 |-  ( ( ( 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 ) ) ) ) )
28 7 27 raleqbidv 
 |-  ( ( ( 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 ) ) ) ) )
29 14 28 rabeqbidv 
 |-  ( ( ( 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 ) ) ) } )
30 6 29 csbied 
 |-  ( ( 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 ) ) ) } )
31 ovex 
 |-  ( Y ^m ( X X. Y ) ) e. _V
32 31 rabex 
 |-  { 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
33 30 4 32 ovmpoa 
 |-  ( ( 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 ) ) ) } )
34 33 eleq2d 
 |-  ( ( 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 ) ) ) } ) )
35 oveq 
 |-  ( m = .(+) -> ( .0. m x ) = ( .0. .(+) x ) )
36 35 eqeq1d 
 |-  ( m = .(+) -> ( ( .0. m x ) = x <-> ( .0. .(+) x ) = x ) )
37 oveq 
 |-  ( m = .(+) -> ( ( y .+ z ) m x ) = ( ( y .+ z ) .(+) x ) )
38 oveq 
 |-  ( m = .(+) -> ( y m ( z m x ) ) = ( y .(+) ( z m x ) ) )
39 oveq 
 |-  ( m = .(+) -> ( z m x ) = ( z .(+) x ) )
40 39 oveq2d 
 |-  ( m = .(+) -> ( y .(+) ( z m x ) ) = ( y .(+) ( z .(+) x ) ) )
41 38 40 eqtrd 
 |-  ( m = .(+) -> ( y m ( z m x ) ) = ( y .(+) ( z .(+) x ) ) )
42 37 41 eqeq12d 
 |-  ( m = .(+) -> ( ( ( y .+ z ) m x ) = ( y m ( z m x ) ) <-> ( ( y .+ z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) )
43 42 2ralbidv 
 |-  ( 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 ) ) ) )
44 36 43 anbi12d 
 |-  ( 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 ) ) ) ) )
45 44 ralbidv 
 |-  ( 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 ) ) ) ) )
46 45 elrab 
 |-  ( .(+) 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 ) ) ) ) )
47 34 46 bitrdi 
 |-  ( ( 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 ) ) ) ) ) )
48 simpr 
 |-  ( ( G e. Grp /\ Y e. _V ) -> Y e. _V )
49 1 fvexi 
 |-  X e. _V
50 xpexg 
 |-  ( ( X e. _V /\ Y e. _V ) -> ( X X. Y ) e. _V )
51 49 48 50 sylancr 
 |-  ( ( G e. Grp /\ Y e. _V ) -> ( X X. Y ) e. _V )
52 48 51 elmapd 
 |-  ( ( G e. Grp /\ Y e. _V ) -> ( .(+) e. ( Y ^m ( X X. Y ) ) <-> .(+) : ( X X. Y ) --> Y ) )
53 52 anbi1d 
 |-  ( ( 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 ) ) ) ) ) )
54 47 53 bitrd 
 |-  ( ( 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 ) ) ) ) ) )
55 5 54 biadanii 
 |-  ( .(+) 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 ) ) ) ) ) )