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 ) ) ) ) ) ) |