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

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