Metamath Proof Explorer


Theorem sylow1lem2

Description: Lemma for sylow1 . The function .(+) is a group action on S . (Contributed by Mario Carneiro, 15-Jan-2015)

Ref Expression
Hypotheses sylow1.x
|- X = ( Base ` G )
sylow1.g
|- ( ph -> G e. Grp )
sylow1.f
|- ( ph -> X e. Fin )
sylow1.p
|- ( ph -> P e. Prime )
sylow1.n
|- ( ph -> N e. NN0 )
sylow1.d
|- ( ph -> ( P ^ N ) || ( # ` X ) )
sylow1lem.a
|- .+ = ( +g ` G )
sylow1lem.s
|- S = { s e. ~P X | ( # ` s ) = ( P ^ N ) }
sylow1lem.m
|- .(+) = ( x e. X , y e. S |-> ran ( z e. y |-> ( x .+ z ) ) )
Assertion sylow1lem2
|- ( ph -> .(+) e. ( G GrpAct S ) )

Proof

Step Hyp Ref Expression
1 sylow1.x
 |-  X = ( Base ` G )
2 sylow1.g
 |-  ( ph -> G e. Grp )
3 sylow1.f
 |-  ( ph -> X e. Fin )
4 sylow1.p
 |-  ( ph -> P e. Prime )
5 sylow1.n
 |-  ( ph -> N e. NN0 )
6 sylow1.d
 |-  ( ph -> ( P ^ N ) || ( # ` X ) )
7 sylow1lem.a
 |-  .+ = ( +g ` G )
8 sylow1lem.s
 |-  S = { s e. ~P X | ( # ` s ) = ( P ^ N ) }
9 sylow1lem.m
 |-  .(+) = ( x e. X , y e. S |-> ran ( z e. y |-> ( x .+ z ) ) )
10 1 fvexi
 |-  X e. _V
11 10 pwex
 |-  ~P X e. _V
12 8 11 rabex2
 |-  S e. _V
13 2 12 jctir
 |-  ( ph -> ( G e. Grp /\ S e. _V ) )
14 simprl
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> x e. X )
15 eqid
 |-  ( z e. X |-> ( x .+ z ) ) = ( z e. X |-> ( x .+ z ) )
16 1 7 15 grplmulf1o
 |-  ( ( G e. Grp /\ x e. X ) -> ( z e. X |-> ( x .+ z ) ) : X -1-1-onto-> X )
17 2 14 16 syl2an2r
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( z e. X |-> ( x .+ z ) ) : X -1-1-onto-> X )
18 f1of1
 |-  ( ( z e. X |-> ( x .+ z ) ) : X -1-1-onto-> X -> ( z e. X |-> ( x .+ z ) ) : X -1-1-> X )
19 17 18 syl
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( z e. X |-> ( x .+ z ) ) : X -1-1-> X )
20 simprr
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> y e. S )
21 fveqeq2
 |-  ( s = y -> ( ( # ` s ) = ( P ^ N ) <-> ( # ` y ) = ( P ^ N ) ) )
22 21 8 elrab2
 |-  ( y e. S <-> ( y e. ~P X /\ ( # ` y ) = ( P ^ N ) ) )
23 20 22 sylib
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( y e. ~P X /\ ( # ` y ) = ( P ^ N ) ) )
24 23 simpld
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> y e. ~P X )
25 24 elpwid
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> y C_ X )
26 f1ssres
 |-  ( ( ( z e. X |-> ( x .+ z ) ) : X -1-1-> X /\ y C_ X ) -> ( ( z e. X |-> ( x .+ z ) ) |` y ) : y -1-1-> X )
27 19 25 26 syl2anc
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( ( z e. X |-> ( x .+ z ) ) |` y ) : y -1-1-> X )
28 resmpt
 |-  ( y C_ X -> ( ( z e. X |-> ( x .+ z ) ) |` y ) = ( z e. y |-> ( x .+ z ) ) )
29 f1eq1
 |-  ( ( ( z e. X |-> ( x .+ z ) ) |` y ) = ( z e. y |-> ( x .+ z ) ) -> ( ( ( z e. X |-> ( x .+ z ) ) |` y ) : y -1-1-> X <-> ( z e. y |-> ( x .+ z ) ) : y -1-1-> X ) )
30 25 28 29 3syl
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( ( ( z e. X |-> ( x .+ z ) ) |` y ) : y -1-1-> X <-> ( z e. y |-> ( x .+ z ) ) : y -1-1-> X ) )
31 27 30 mpbid
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( z e. y |-> ( x .+ z ) ) : y -1-1-> X )
32 f1f
 |-  ( ( z e. y |-> ( x .+ z ) ) : y -1-1-> X -> ( z e. y |-> ( x .+ z ) ) : y --> X )
33 frn
 |-  ( ( z e. y |-> ( x .+ z ) ) : y --> X -> ran ( z e. y |-> ( x .+ z ) ) C_ X )
34 31 32 33 3syl
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ran ( z e. y |-> ( x .+ z ) ) C_ X )
35 10 elpw2
 |-  ( ran ( z e. y |-> ( x .+ z ) ) e. ~P X <-> ran ( z e. y |-> ( x .+ z ) ) C_ X )
36 34 35 sylibr
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ran ( z e. y |-> ( x .+ z ) ) e. ~P X )
37 f1f1orn
 |-  ( ( z e. y |-> ( x .+ z ) ) : y -1-1-> X -> ( z e. y |-> ( x .+ z ) ) : y -1-1-onto-> ran ( z e. y |-> ( x .+ z ) ) )
38 vex
 |-  y e. _V
39 38 f1oen
 |-  ( ( z e. y |-> ( x .+ z ) ) : y -1-1-onto-> ran ( z e. y |-> ( x .+ z ) ) -> y ~~ ran ( z e. y |-> ( x .+ z ) ) )
40 31 37 39 3syl
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> y ~~ ran ( z e. y |-> ( x .+ z ) ) )
41 ssfi
 |-  ( ( X e. Fin /\ y C_ X ) -> y e. Fin )
42 3 25 41 syl2an2r
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> y e. Fin )
43 ssfi
 |-  ( ( X e. Fin /\ ran ( z e. y |-> ( x .+ z ) ) C_ X ) -> ran ( z e. y |-> ( x .+ z ) ) e. Fin )
44 3 34 43 syl2an2r
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ran ( z e. y |-> ( x .+ z ) ) e. Fin )
45 hashen
 |-  ( ( y e. Fin /\ ran ( z e. y |-> ( x .+ z ) ) e. Fin ) -> ( ( # ` y ) = ( # ` ran ( z e. y |-> ( x .+ z ) ) ) <-> y ~~ ran ( z e. y |-> ( x .+ z ) ) ) )
46 42 44 45 syl2anc
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( ( # ` y ) = ( # ` ran ( z e. y |-> ( x .+ z ) ) ) <-> y ~~ ran ( z e. y |-> ( x .+ z ) ) ) )
47 40 46 mpbird
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( # ` y ) = ( # ` ran ( z e. y |-> ( x .+ z ) ) ) )
48 23 simprd
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( # ` y ) = ( P ^ N ) )
49 47 48 eqtr3d
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ( # ` ran ( z e. y |-> ( x .+ z ) ) ) = ( P ^ N ) )
50 fveqeq2
 |-  ( s = ran ( z e. y |-> ( x .+ z ) ) -> ( ( # ` s ) = ( P ^ N ) <-> ( # ` ran ( z e. y |-> ( x .+ z ) ) ) = ( P ^ N ) ) )
51 50 8 elrab2
 |-  ( ran ( z e. y |-> ( x .+ z ) ) e. S <-> ( ran ( z e. y |-> ( x .+ z ) ) e. ~P X /\ ( # ` ran ( z e. y |-> ( x .+ z ) ) ) = ( P ^ N ) ) )
52 36 49 51 sylanbrc
 |-  ( ( ph /\ ( x e. X /\ y e. S ) ) -> ran ( z e. y |-> ( x .+ z ) ) e. S )
53 52 ralrimivva
 |-  ( ph -> A. x e. X A. y e. S ran ( z e. y |-> ( x .+ z ) ) e. S )
54 9 fmpo
 |-  ( A. x e. X A. y e. S ran ( z e. y |-> ( x .+ z ) ) e. S <-> .(+) : ( X X. S ) --> S )
55 53 54 sylib
 |-  ( ph -> .(+) : ( X X. S ) --> S )
56 2 adantr
 |-  ( ( ph /\ a e. S ) -> G e. Grp )
57 eqid
 |-  ( 0g ` G ) = ( 0g ` G )
58 1 57 grpidcl
 |-  ( G e. Grp -> ( 0g ` G ) e. X )
59 56 58 syl
 |-  ( ( ph /\ a e. S ) -> ( 0g ` G ) e. X )
60 simpr
 |-  ( ( ph /\ a e. S ) -> a e. S )
61 simpr
 |-  ( ( x = ( 0g ` G ) /\ y = a ) -> y = a )
62 simpl
 |-  ( ( x = ( 0g ` G ) /\ y = a ) -> x = ( 0g ` G ) )
63 62 oveq1d
 |-  ( ( x = ( 0g ` G ) /\ y = a ) -> ( x .+ z ) = ( ( 0g ` G ) .+ z ) )
64 61 63 mpteq12dv
 |-  ( ( x = ( 0g ` G ) /\ y = a ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
65 64 rneqd
 |-  ( ( x = ( 0g ` G ) /\ y = a ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
66 vex
 |-  a e. _V
67 66 mptex
 |-  ( z e. a |-> ( ( 0g ` G ) .+ z ) ) e. _V
68 67 rnex
 |-  ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) e. _V
69 65 9 68 ovmpoa
 |-  ( ( ( 0g ` G ) e. X /\ a e. S ) -> ( ( 0g ` G ) .(+) a ) = ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
70 59 60 69 syl2anc
 |-  ( ( ph /\ a e. S ) -> ( ( 0g ` G ) .(+) a ) = ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) )
71 8 ssrab3
 |-  S C_ ~P X
72 71 60 sselid
 |-  ( ( ph /\ a e. S ) -> a e. ~P X )
73 72 elpwid
 |-  ( ( ph /\ a e. S ) -> a C_ X )
74 73 sselda
 |-  ( ( ( ph /\ a e. S ) /\ z e. a ) -> z e. X )
75 1 7 57 grplid
 |-  ( ( G e. Grp /\ z e. X ) -> ( ( 0g ` G ) .+ z ) = z )
76 56 74 75 syl2an2r
 |-  ( ( ( ph /\ a e. S ) /\ z e. a ) -> ( ( 0g ` G ) .+ z ) = z )
77 76 mpteq2dva
 |-  ( ( ph /\ a e. S ) -> ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = ( z e. a |-> z ) )
78 mptresid
 |-  ( _I |` a ) = ( z e. a |-> z )
79 77 78 eqtr4di
 |-  ( ( ph /\ a e. S ) -> ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = ( _I |` a ) )
80 79 rneqd
 |-  ( ( ph /\ a e. S ) -> ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = ran ( _I |` a ) )
81 rnresi
 |-  ran ( _I |` a ) = a
82 80 81 eqtrdi
 |-  ( ( ph /\ a e. S ) -> ran ( z e. a |-> ( ( 0g ` G ) .+ z ) ) = a )
83 70 82 eqtrd
 |-  ( ( ph /\ a e. S ) -> ( ( 0g ` G ) .(+) a ) = a )
84 ovex
 |-  ( c .+ z ) e. _V
85 oveq2
 |-  ( w = ( c .+ z ) -> ( b .+ w ) = ( b .+ ( c .+ z ) ) )
86 84 85 abrexco
 |-  { u | E. w e. { v | E. z e. a v = ( c .+ z ) } u = ( b .+ w ) } = { u | E. z e. a u = ( b .+ ( c .+ z ) ) }
87 simprr
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> c e. X )
88 60 adantr
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> a e. S )
89 simpr
 |-  ( ( x = c /\ y = a ) -> y = a )
90 simpl
 |-  ( ( x = c /\ y = a ) -> x = c )
91 90 oveq1d
 |-  ( ( x = c /\ y = a ) -> ( x .+ z ) = ( c .+ z ) )
92 89 91 mpteq12dv
 |-  ( ( x = c /\ y = a ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. a |-> ( c .+ z ) ) )
93 92 rneqd
 |-  ( ( x = c /\ y = a ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. a |-> ( c .+ z ) ) )
94 66 mptex
 |-  ( z e. a |-> ( c .+ z ) ) e. _V
95 94 rnex
 |-  ran ( z e. a |-> ( c .+ z ) ) e. _V
96 93 9 95 ovmpoa
 |-  ( ( c e. X /\ a e. S ) -> ( c .(+) a ) = ran ( z e. a |-> ( c .+ z ) ) )
97 87 88 96 syl2anc
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) = ran ( z e. a |-> ( c .+ z ) ) )
98 eqid
 |-  ( z e. a |-> ( c .+ z ) ) = ( z e. a |-> ( c .+ z ) )
99 98 rnmpt
 |-  ran ( z e. a |-> ( c .+ z ) ) = { v | E. z e. a v = ( c .+ z ) }
100 97 99 eqtrdi
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) = { v | E. z e. a v = ( c .+ z ) } )
101 100 rexeqdv
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( E. w e. ( c .(+) a ) u = ( b .+ w ) <-> E. w e. { v | E. z e. a v = ( c .+ z ) } u = ( b .+ w ) ) )
102 101 abbidv
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> { u | E. w e. ( c .(+) a ) u = ( b .+ w ) } = { u | E. w e. { v | E. z e. a v = ( c .+ z ) } u = ( b .+ w ) } )
103 56 ad2antrr
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> G e. Grp )
104 simprl
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> b e. X )
105 104 adantr
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> b e. X )
106 87 adantr
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> c e. X )
107 74 adantlr
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> z e. X )
108 1 7 grpass
 |-  ( ( G e. Grp /\ ( b e. X /\ c e. X /\ z e. X ) ) -> ( ( b .+ c ) .+ z ) = ( b .+ ( c .+ z ) ) )
109 103 105 106 107 108 syl13anc
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( ( b .+ c ) .+ z ) = ( b .+ ( c .+ z ) ) )
110 109 eqeq2d
 |-  ( ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) /\ z e. a ) -> ( u = ( ( b .+ c ) .+ z ) <-> u = ( b .+ ( c .+ z ) ) ) )
111 110 rexbidva
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( E. z e. a u = ( ( b .+ c ) .+ z ) <-> E. z e. a u = ( b .+ ( c .+ z ) ) ) )
112 111 abbidv
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> { u | E. z e. a u = ( ( b .+ c ) .+ z ) } = { u | E. z e. a u = ( b .+ ( c .+ z ) ) } )
113 86 102 112 3eqtr4a
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> { u | E. w e. ( c .(+) a ) u = ( b .+ w ) } = { u | E. z e. a u = ( ( b .+ c ) .+ z ) } )
114 eqid
 |-  ( w e. ( c .(+) a ) |-> ( b .+ w ) ) = ( w e. ( c .(+) a ) |-> ( b .+ w ) )
115 114 rnmpt
 |-  ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) = { u | E. w e. ( c .(+) a ) u = ( b .+ w ) }
116 eqid
 |-  ( z e. a |-> ( ( b .+ c ) .+ z ) ) = ( z e. a |-> ( ( b .+ c ) .+ z ) )
117 116 rnmpt
 |-  ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) = { u | E. z e. a u = ( ( b .+ c ) .+ z ) }
118 113 115 117 3eqtr4g
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) = ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
119 55 ad2antrr
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> .(+) : ( X X. S ) --> S )
120 119 87 88 fovrnd
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( c .(+) a ) e. S )
121 simpr
 |-  ( ( x = b /\ y = ( c .(+) a ) ) -> y = ( c .(+) a ) )
122 simpl
 |-  ( ( x = b /\ y = ( c .(+) a ) ) -> x = b )
123 122 oveq1d
 |-  ( ( x = b /\ y = ( c .(+) a ) ) -> ( x .+ z ) = ( b .+ z ) )
124 121 123 mpteq12dv
 |-  ( ( x = b /\ y = ( c .(+) a ) ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. ( c .(+) a ) |-> ( b .+ z ) ) )
125 oveq2
 |-  ( z = w -> ( b .+ z ) = ( b .+ w ) )
126 125 cbvmptv
 |-  ( z e. ( c .(+) a ) |-> ( b .+ z ) ) = ( w e. ( c .(+) a ) |-> ( b .+ w ) )
127 124 126 eqtrdi
 |-  ( ( x = b /\ y = ( c .(+) a ) ) -> ( z e. y |-> ( x .+ z ) ) = ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
128 127 rneqd
 |-  ( ( x = b /\ y = ( c .(+) a ) ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
129 ovex
 |-  ( c .(+) a ) e. _V
130 129 mptex
 |-  ( w e. ( c .(+) a ) |-> ( b .+ w ) ) e. _V
131 130 rnex
 |-  ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) e. _V
132 128 9 131 ovmpoa
 |-  ( ( b e. X /\ ( c .(+) a ) e. S ) -> ( b .(+) ( c .(+) a ) ) = ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
133 104 120 132 syl2anc
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( b .(+) ( c .(+) a ) ) = ran ( w e. ( c .(+) a ) |-> ( b .+ w ) ) )
134 2 ad2antrr
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> G e. Grp )
135 1 7 grpcl
 |-  ( ( G e. Grp /\ b e. X /\ c e. X ) -> ( b .+ c ) e. X )
136 134 104 87 135 syl3anc
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( b .+ c ) e. X )
137 simpr
 |-  ( ( x = ( b .+ c ) /\ y = a ) -> y = a )
138 simpl
 |-  ( ( x = ( b .+ c ) /\ y = a ) -> x = ( b .+ c ) )
139 138 oveq1d
 |-  ( ( x = ( b .+ c ) /\ y = a ) -> ( x .+ z ) = ( ( b .+ c ) .+ z ) )
140 137 139 mpteq12dv
 |-  ( ( x = ( b .+ c ) /\ y = a ) -> ( z e. y |-> ( x .+ z ) ) = ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
141 140 rneqd
 |-  ( ( x = ( b .+ c ) /\ y = a ) -> ran ( z e. y |-> ( x .+ z ) ) = ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
142 66 mptex
 |-  ( z e. a |-> ( ( b .+ c ) .+ z ) ) e. _V
143 142 rnex
 |-  ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) e. _V
144 141 9 143 ovmpoa
 |-  ( ( ( b .+ c ) e. X /\ a e. S ) -> ( ( b .+ c ) .(+) a ) = ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
145 136 88 144 syl2anc
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( ( b .+ c ) .(+) a ) = ran ( z e. a |-> ( ( b .+ c ) .+ z ) ) )
146 118 133 145 3eqtr4rd
 |-  ( ( ( ph /\ a e. S ) /\ ( b e. X /\ c e. X ) ) -> ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) )
147 146 ralrimivva
 |-  ( ( ph /\ a e. S ) -> A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) )
148 83 147 jca
 |-  ( ( ph /\ a e. S ) -> ( ( ( 0g ` G ) .(+) a ) = a /\ A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) ) )
149 148 ralrimiva
 |-  ( ph -> A. a e. S ( ( ( 0g ` G ) .(+) a ) = a /\ A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) ) )
150 55 149 jca
 |-  ( ph -> ( .(+) : ( X X. S ) --> S /\ A. a e. S ( ( ( 0g ` G ) .(+) a ) = a /\ A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) ) ) )
151 1 7 57 isga
 |-  ( .(+) e. ( G GrpAct S ) <-> ( ( G e. Grp /\ S e. _V ) /\ ( .(+) : ( X X. S ) --> S /\ A. a e. S ( ( ( 0g ` G ) .(+) a ) = a /\ A. b e. X A. c e. X ( ( b .+ c ) .(+) a ) = ( b .(+) ( c .(+) a ) ) ) ) ) )
152 13 150 151 sylanbrc
 |-  ( ph -> .(+) e. ( G GrpAct S ) )