Metamath Proof Explorer

Theorem sylow3lem1

Description: Lemma for sylow3 , first part. (Contributed by Mario Carneiro, 19-Jan-2015)

Ref Expression
Hypotheses sylow3.x 
|- X = ( Base ` G )
sylow3.g 
|- ( ph -> G e. Grp )
sylow3.xf 
|- ( ph -> X e. Fin )
sylow3.p 
|- ( ph -> P e. Prime )
sylow3lem1.a 
|- .+ = ( +g ` G )
sylow3lem1.d 
|- .- = ( -g ` G )
sylow3lem1.m 
|- .(+) = ( x e. X , y e. ( P pSyl G ) |-> ran ( z e. y |-> ( ( x .+ z ) .- x ) ) )
Assertion sylow3lem1 
|- ( ph -> .(+) e. ( G GrpAct ( P pSyl G ) ) )

Proof

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