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

Metamath Proof Explorer

Theorem sylow2blem3

Description: Sylow's second theorem. Putting together the results of sylow2a and the orbit-stabilizer theorem to show that P does not divide the set of all fixed points under the group action, we get that there is a fixed point of the group action, so that there is some g e. X with h g K = g K for all h e. H . This implies that invg ( g ) h g e. K , so h is in the conjugated subgroup g K invg ( g ) . (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses sylow2b.x 
|- X = ( Base ` G )
sylow2b.xf 
|- ( ph -> X e. Fin )
sylow2b.h 
|- ( ph -> H e. ( SubGrp ` G ) )
sylow2b.k 
|- ( ph -> K e. ( SubGrp ` G ) )
sylow2b.a 
|- .+ = ( +g ` G )
sylow2b.r 
|- .~ = ( G ~QG K )
sylow2b.m 
|- .x. = ( x e. H , y e. ( X /. .~ ) |-> ran ( z e. y |-> ( x .+ z ) ) )
sylow2blem3.hp 
|- ( ph -> P pGrp ( G |`s H ) )
sylow2blem3.kn 
|- ( ph -> ( # ` K ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
sylow2blem3.d 
|- .- = ( -g ` G )
Assertion sylow2blem3 
|- ( ph -> E. g e. X H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )

Proof

Step Hyp Ref Expression
1 sylow2b.x 
 |-  X = ( Base ` G )
2 sylow2b.xf 
 |-  ( ph -> X e. Fin )
3 sylow2b.h 
 |-  ( ph -> H e. ( SubGrp ` G ) )
4 sylow2b.k 
 |-  ( ph -> K e. ( SubGrp ` G ) )
5 sylow2b.a 
 |-  .+ = ( +g ` G )
6 sylow2b.r 
 |-  .~ = ( G ~QG K )
7 sylow2b.m 
 |-  .x. = ( x e. H , y e. ( X /. .~ ) |-> ran ( z e. y |-> ( x .+ z ) ) )
8 sylow2blem3.hp 
 |-  ( ph -> P pGrp ( G |`s H ) )
9 sylow2blem3.kn 
 |-  ( ph -> ( # ` K ) = ( P ^ ( P pCnt ( # ` X ) ) ) )
10 sylow2blem3.d 
 |-  .- = ( -g ` G )
11 pgpprm 
 |-  ( P pGrp ( G |`s H ) -> P e. Prime )
12 8 11 syl 
 |-  ( ph -> P e. Prime )
13 subgrcl 
 |-  ( H e. ( SubGrp ` G ) -> G e. Grp )
14 3 13 syl 
 |-  ( ph -> G e. Grp )
15 1 grpbn0 
 |-  ( G e. Grp -> X =/= (/) )
16 14 15 syl 
 |-  ( ph -> X =/= (/) )
17 hashnncl 
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
18 2 17 syl 
 |-  ( ph -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
19 16 18 mpbird 
 |-  ( ph -> ( # ` X ) e. NN )
20 pcndvds2 
 |-  ( ( P e. Prime /\ ( # ` X ) e. NN ) -> -. P || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) )
21 12 19 20 syl2anc 
 |-  ( ph -> -. P || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) )
22 1 6 4 2 lagsubg2 
 |-  ( ph -> ( # ` X ) = ( ( # ` ( X /. .~ ) ) x. ( # ` K ) ) )
23 22 oveq1d 
 |-  ( ph -> ( ( # ` X ) / ( # ` K ) ) = ( ( ( # ` ( X /. .~ ) ) x. ( # ` K ) ) / ( # ` K ) ) )
24 9 oveq2d 
 |-  ( ph -> ( ( # ` X ) / ( # ` K ) ) = ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) )
25 pwfi 
 |-  ( X e. Fin <-> ~P X e. Fin )
26 2 25 sylib 
 |-  ( ph -> ~P X e. Fin )
27 1 6 eqger 
 |-  ( K e. ( SubGrp ` G ) -> .~ Er X )
28 4 27 syl 
 |-  ( ph -> .~ Er X )
29 28 qsss 
 |-  ( ph -> ( X /. .~ ) C_ ~P X )
30 26 29 ssfid 
 |-  ( ph -> ( X /. .~ ) e. Fin )
31 hashcl 
 |-  ( ( X /. .~ ) e. Fin -> ( # ` ( X /. .~ ) ) e. NN0 )
32 30 31 syl 
 |-  ( ph -> ( # ` ( X /. .~ ) ) e. NN0 )
33 32 nn0cnd 
 |-  ( ph -> ( # ` ( X /. .~ ) ) e. CC )
34 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
35 34 subg0cl 
 |-  ( K e. ( SubGrp ` G ) -> ( 0g ` G ) e. K )
36 4 35 syl 
 |-  ( ph -> ( 0g ` G ) e. K )
37 36 ne0d 
 |-  ( ph -> K =/= (/) )
38 1 subgss 
 |-  ( K e. ( SubGrp ` G ) -> K C_ X )
39 4 38 syl 
 |-  ( ph -> K C_ X )
40 2 39 ssfid 
 |-  ( ph -> K e. Fin )
41 hashnncl 
 |-  ( K e. Fin -> ( ( # ` K ) e. NN <-> K =/= (/) ) )
42 40 41 syl 
 |-  ( ph -> ( ( # ` K ) e. NN <-> K =/= (/) ) )
43 37 42 mpbird 
 |-  ( ph -> ( # ` K ) e. NN )
44 43 nncnd 
 |-  ( ph -> ( # ` K ) e. CC )
45 43 nnne0d 
 |-  ( ph -> ( # ` K ) =/= 0 )
46 33 44 45 divcan4d 
 |-  ( ph -> ( ( ( # ` ( X /. .~ ) ) x. ( # ` K ) ) / ( # ` K ) ) = ( # ` ( X /. .~ ) ) )
47 23 24 46 3eqtr3d 
 |-  ( ph -> ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) = ( # ` ( X /. .~ ) ) )
48 47 breq2d 
 |-  ( ph -> ( P || ( ( # ` X ) / ( P ^ ( P pCnt ( # ` X ) ) ) ) <-> P || ( # ` ( X /. .~ ) ) ) )
49 21 48 mtbid 
 |-  ( ph -> -. P || ( # ` ( X /. .~ ) ) )
50 prmz 
 |-  ( P e. Prime -> P e. ZZ )
51 12 50 syl 
 |-  ( ph -> P e. ZZ )
52 32 nn0zd 
 |-  ( ph -> ( # ` ( X /. .~ ) ) e. ZZ )
53 ssrab2 
 |-  { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } C_ ( X /. .~ )
54 ssfi 
 |-  ( ( ( X /. .~ ) e. Fin /\ { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } C_ ( X /. .~ ) ) -> { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } e. Fin )
55 30 53 54 sylancl 
 |-  ( ph -> { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } e. Fin )
56 hashcl 
 |-  ( { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } e. Fin -> ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) e. NN0 )
57 55 56 syl 
 |-  ( ph -> ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) e. NN0 )
58 57 nn0zd 
 |-  ( ph -> ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) e. ZZ )
59 eqid 
 |-  ( Base ` ( G |`s H ) ) = ( Base ` ( G |`s H ) )
60 1 2 3 4 5 6 7 sylow2blem2 
 |-  ( ph -> .x. e. ( ( G |`s H ) GrpAct ( X /. .~ ) ) )
61 eqid 
 |-  ( G |`s H ) = ( G |`s H )
62 61 subgbas 
 |-  ( H e. ( SubGrp ` G ) -> H = ( Base ` ( G |`s H ) ) )
63 3 62 syl 
 |-  ( ph -> H = ( Base ` ( G |`s H ) ) )
64 1 subgss 
 |-  ( H e. ( SubGrp ` G ) -> H C_ X )
65 3 64 syl 
 |-  ( ph -> H C_ X )
66 2 65 ssfid 
 |-  ( ph -> H e. Fin )
67 63 66 eqeltrrd 
 |-  ( ph -> ( Base ` ( G |`s H ) ) e. Fin )
68 eqid 
 |-  { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } = { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z }
69 eqid 
 |-  { <. x , y >. | ( { x , y } C_ ( X /. .~ ) /\ E. g e. ( Base ` ( G |`s H ) ) ( g .x. x ) = y ) } = { <. x , y >. | ( { x , y } C_ ( X /. .~ ) /\ E. g e. ( Base ` ( G |`s H ) ) ( g .x. x ) = y ) }
70 59 60 8 67 30 68 69 sylow2a 
 |-  ( ph -> P || ( ( # ` ( X /. .~ ) ) - ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) ) )
71 dvdssub2 
 |-  ( ( ( P e. ZZ /\ ( # ` ( X /. .~ ) ) e. ZZ /\ ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) e. ZZ ) /\ P || ( ( # ` ( X /. .~ ) ) - ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) ) ) -> ( P || ( # ` ( X /. .~ ) ) <-> P || ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) ) )
72 51 52 58 70 71 syl31anc 
 |-  ( ph -> ( P || ( # ` ( X /. .~ ) ) <-> P || ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) ) )
73 49 72 mtbid 
 |-  ( ph -> -. P || ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) )
74 hasheq0 
 |-  ( { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } e. Fin -> ( ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) = 0 <-> { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } = (/) ) )
75 55 74 syl 
 |-  ( ph -> ( ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) = 0 <-> { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } = (/) ) )
76 dvds0 
 |-  ( P e. ZZ -> P || 0 )
77 51 76 syl 
 |-  ( ph -> P || 0 )
78 breq2 
 |-  ( ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) = 0 -> ( P || ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) <-> P || 0 ) )
79 77 78 syl5ibrcom 
 |-  ( ph -> ( ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) = 0 -> P || ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) ) )
80 75 79 sylbird 
 |-  ( ph -> ( { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } = (/) -> P || ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) ) )
81 80 necon3bd 
 |-  ( ph -> ( -. P || ( # ` { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } ) -> { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } =/= (/) ) )
82 73 81 mpd 
 |-  ( ph -> { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } =/= (/) )
83 rabn0 
 |-  ( { z e. ( X /. .~ ) | A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z } =/= (/) <-> E. z e. ( X /. .~ ) A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z )
84 82 83 sylib 
 |-  ( ph -> E. z e. ( X /. .~ ) A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z )
85 63 raleqdv 
 |-  ( ph -> ( A. u e. H ( u .x. z ) = z <-> A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z ) )
86 85 rexbidv 
 |-  ( ph -> ( E. z e. ( X /. .~ ) A. u e. H ( u .x. z ) = z <-> E. z e. ( X /. .~ ) A. u e. ( Base ` ( G |`s H ) ) ( u .x. z ) = z ) )
87 84 86 mpbird 
 |-  ( ph -> E. z e. ( X /. .~ ) A. u e. H ( u .x. z ) = z )
88 vex 
 |-  z e. _V
89 88 elqs 
 |-  ( z e. ( X /. .~ ) <-> E. g e. X z = [ g ] .~ )
90 simplrr 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> z = [ g ] .~ )
91 90 oveq2d 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( u .x. z ) = ( u .x. [ g ] .~ ) )
92 simprr 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( u .x. z ) = z )
93 simpll 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ph )
94 simprl 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> u e. H )
95 simplrl 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> g e. X )
96 1 2 3 4 5 6 7 sylow2blem1 
 |-  ( ( ph /\ u e. H /\ g e. X ) -> ( u .x. [ g ] .~ ) = [ ( u .+ g ) ] .~ )
97 93 94 95 96 syl3anc 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( u .x. [ g ] .~ ) = [ ( u .+ g ) ] .~ )
98 91 92 97 3eqtr3d 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> z = [ ( u .+ g ) ] .~ )
99 90 98 eqtr3d 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> [ g ] .~ = [ ( u .+ g ) ] .~ )
100 28 ad2antrr 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> .~ Er X )
101 100 95 erth 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( g .~ ( u .+ g ) <-> [ g ] .~ = [ ( u .+ g ) ] .~ ) )
102 99 101 mpbird 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> g .~ ( u .+ g ) )
103 14 ad2antrr 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> G e. Grp )
104 39 ad2antrr 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> K C_ X )
105 eqid 
 |-  ( invg ` G ) = ( invg ` G )
106 1 105 5 6 eqgval 
 |-  ( ( G e. Grp /\ K C_ X ) -> ( g .~ ( u .+ g ) <-> ( g e. X /\ ( u .+ g ) e. X /\ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) e. K ) ) )
107 103 104 106 syl2anc 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( g .~ ( u .+ g ) <-> ( g e. X /\ ( u .+ g ) e. X /\ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) e. K ) ) )
108 102 107 mpbid 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( g e. X /\ ( u .+ g ) e. X /\ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) e. K ) )
109 108 simp3d 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) e. K )
110 oveq2 
 |-  ( x = ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) -> ( g .+ x ) = ( g .+ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) )
111 110 oveq1d 
 |-  ( x = ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) -> ( ( g .+ x ) .- g ) = ( ( g .+ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) .- g ) )
112 eqid 
 |-  ( x e. K |-> ( ( g .+ x ) .- g ) ) = ( x e. K |-> ( ( g .+ x ) .- g ) )
113 ovex 
 |-  ( ( g .+ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) .- g ) e. _V
114 111 112 113 fvmpt 
 |-  ( ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) e. K -> ( ( x e. K |-> ( ( g .+ x ) .- g ) ) ` ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) = ( ( g .+ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) .- g ) )
115 109 114 syl 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( ( x e. K |-> ( ( g .+ x ) .- g ) ) ` ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) = ( ( g .+ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) .- g ) )
116 1 5 34 105 grprinv 
 |-  ( ( G e. Grp /\ g e. X ) -> ( g .+ ( ( invg ` G ) ` g ) ) = ( 0g ` G ) )
117 103 95 116 syl2anc 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( g .+ ( ( invg ` G ) ` g ) ) = ( 0g ` G ) )
118 117 oveq1d 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( ( g .+ ( ( invg ` G ) ` g ) ) .+ ( u .+ g ) ) = ( ( 0g ` G ) .+ ( u .+ g ) ) )
119 1 105 grpinvcl 
 |-  ( ( G e. Grp /\ g e. X ) -> ( ( invg ` G ) ` g ) e. X )
120 103 95 119 syl2anc 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( ( invg ` G ) ` g ) e. X )
121 65 ad2antrr 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> H C_ X )
122 121 94 sseldd 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> u e. X )
123 1 5 grpcl 
 |-  ( ( G e. Grp /\ u e. X /\ g e. X ) -> ( u .+ g ) e. X )
124 103 122 95 123 syl3anc 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( u .+ g ) e. X )
125 1 5 grpass 
 |-  ( ( G e. Grp /\ ( g e. X /\ ( ( invg ` G ) ` g ) e. X /\ ( u .+ g ) e. X ) ) -> ( ( g .+ ( ( invg ` G ) ` g ) ) .+ ( u .+ g ) ) = ( g .+ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) )
126 103 95 120 124 125 syl13anc 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( ( g .+ ( ( invg ` G ) ` g ) ) .+ ( u .+ g ) ) = ( g .+ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) )
127 1 5 34 grplid 
 |-  ( ( G e. Grp /\ ( u .+ g ) e. X ) -> ( ( 0g ` G ) .+ ( u .+ g ) ) = ( u .+ g ) )
128 103 124 127 syl2anc 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( ( 0g ` G ) .+ ( u .+ g ) ) = ( u .+ g ) )
129 118 126 128 3eqtr3d 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( g .+ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) = ( u .+ g ) )
130 129 oveq1d 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( ( g .+ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) .- g ) = ( ( u .+ g ) .- g ) )
131 1 5 10 grppncan 
 |-  ( ( G e. Grp /\ u e. X /\ g e. X ) -> ( ( u .+ g ) .- g ) = u )
132 103 122 95 131 syl3anc 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( ( u .+ g ) .- g ) = u )
133 115 130 132 3eqtrd 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( ( x e. K |-> ( ( g .+ x ) .- g ) ) ` ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) = u )
134 ovex 
 |-  ( ( g .+ x ) .- g ) e. _V
135 134 112 fnmpti 
 |-  ( x e. K |-> ( ( g .+ x ) .- g ) ) Fn K
136 fnfvelrn 
 |-  ( ( ( x e. K |-> ( ( g .+ x ) .- g ) ) Fn K /\ ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) e. K ) -> ( ( x e. K |-> ( ( g .+ x ) .- g ) ) ` ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) e. ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
137 135 109 136 sylancr 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> ( ( x e. K |-> ( ( g .+ x ) .- g ) ) ` ( ( ( invg ` G ) ` g ) .+ ( u .+ g ) ) ) e. ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
138 133 137 eqeltrrd 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ ( u e. H /\ ( u .x. z ) = z ) ) -> u e. ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
139 138 expr 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ u e. H ) -> ( ( u .x. z ) = z -> u e. ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) )
140 139 ralimdva 
 |-  ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) -> ( A. u e. H ( u .x. z ) = z -> A. u e. H u e. ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) )
141 140 imp 
 |-  ( ( ( ph /\ ( g e. X /\ z = [ g ] .~ ) ) /\ A. u e. H ( u .x. z ) = z ) -> A. u e. H u e. ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
142 141 an32s 
 |-  ( ( ( ph /\ A. u e. H ( u .x. z ) = z ) /\ ( g e. X /\ z = [ g ] .~ ) ) -> A. u e. H u e. ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
143 dfss3 
 |-  ( H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) <-> A. u e. H u e. ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
144 142 143 sylibr 
 |-  ( ( ( ph /\ A. u e. H ( u .x. z ) = z ) /\ ( g e. X /\ z = [ g ] .~ ) ) -> H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )
145 144 expr 
 |-  ( ( ( ph /\ A. u e. H ( u .x. z ) = z ) /\ g e. X ) -> ( z = [ g ] .~ -> H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) )
146 145 reximdva 
 |-  ( ( ph /\ A. u e. H ( u .x. z ) = z ) -> ( E. g e. X z = [ g ] .~ -> E. g e. X H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) )
147 146 ex 
 |-  ( ph -> ( A. u e. H ( u .x. z ) = z -> ( E. g e. X z = [ g ] .~ -> E. g e. X H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) ) )
148 147 com23 
 |-  ( ph -> ( E. g e. X z = [ g ] .~ -> ( A. u e. H ( u .x. z ) = z -> E. g e. X H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) ) )
149 89 148 biimtrid 
 |-  ( ph -> ( z e. ( X /. .~ ) -> ( A. u e. H ( u .x. z ) = z -> E. g e. X H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) ) )
150 149 rexlimdv 
 |-  ( ph -> ( E. z e. ( X /. .~ ) A. u e. H ( u .x. z ) = z -> E. g e. X H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) ) )
151 87 150 mpd 
 |-  ( ph -> E. g e. X H C_ ran ( x e. K |-> ( ( g .+ x ) .- g ) ) )