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=BaseG
sylow2b.xf φXFin
sylow2b.h φHSubGrpG
sylow2b.k φKSubGrpG
sylow2b.a +˙=+G
sylow2b.r ˙=G~QGK
sylow2b.m ·˙=xH,yX/˙ranzyx+˙z
sylow2blem3.hp φPpGrpG𝑠H
sylow2blem3.kn φK=PPpCntX
sylow2blem3.d -˙=-G
Assertion sylow2blem3 φgXHranxKg+˙x-˙g

Proof

Step Hyp Ref Expression
1 sylow2b.x X=BaseG
2 sylow2b.xf φXFin
3 sylow2b.h φHSubGrpG
4 sylow2b.k φKSubGrpG
5 sylow2b.a +˙=+G
6 sylow2b.r ˙=G~QGK
7 sylow2b.m ·˙=xH,yX/˙ranzyx+˙z
8 sylow2blem3.hp φPpGrpG𝑠H
9 sylow2blem3.kn φK=PPpCntX
10 sylow2blem3.d -˙=-G
11 pgpprm PpGrpG𝑠HP
12 8 11 syl φP
13 subgrcl HSubGrpGGGrp
14 3 13 syl φGGrp
15 1 grpbn0 GGrpX
16 14 15 syl φX
17 hashnncl XFinXX
18 2 17 syl φXX
19 16 18 mpbird φX
20 pcndvds2 PX¬PXPPpCntX
21 12 19 20 syl2anc φ¬PXPPpCntX
22 1 6 4 2 lagsubg2 φX=X/˙K
23 22 oveq1d φXK=X/˙KK
24 9 oveq2d φXK=XPPpCntX
25 pwfi XFin𝒫XFin
26 2 25 sylib φ𝒫XFin
27 1 6 eqger KSubGrpG˙ErX
28 4 27 syl φ˙ErX
29 28 qsss φX/˙𝒫X
30 26 29 ssfid φX/˙Fin
31 hashcl X/˙FinX/˙0
32 30 31 syl φX/˙0
33 32 nn0cnd φX/˙
34 eqid 0G=0G
35 34 subg0cl KSubGrpG0GK
36 4 35 syl φ0GK
37 36 ne0d φK
38 1 subgss KSubGrpGKX
39 4 38 syl φKX
40 2 39 ssfid φKFin
41 hashnncl KFinKK
42 40 41 syl φKK
43 37 42 mpbird φK
44 43 nncnd φK
45 43 nnne0d φK0
46 33 44 45 divcan4d φX/˙KK=X/˙
47 23 24 46 3eqtr3d φXPPpCntX=X/˙
48 47 breq2d φPXPPpCntXPX/˙
49 21 48 mtbid φ¬PX/˙
50 prmz PP
51 12 50 syl φP
52 32 nn0zd φX/˙
53 ssrab2 zX/˙|uBaseG𝑠Hu·˙z=zX/˙
54 ssfi X/˙FinzX/˙|uBaseG𝑠Hu·˙z=zX/˙zX/˙|uBaseG𝑠Hu·˙z=zFin
55 30 53 54 sylancl φzX/˙|uBaseG𝑠Hu·˙z=zFin
56 hashcl zX/˙|uBaseG𝑠Hu·˙z=zFinzX/˙|uBaseG𝑠Hu·˙z=z0
57 55 56 syl φzX/˙|uBaseG𝑠Hu·˙z=z0
58 57 nn0zd φzX/˙|uBaseG𝑠Hu·˙z=z
59 eqid BaseG𝑠H=BaseG𝑠H
60 1 2 3 4 5 6 7 sylow2blem2 φ·˙G𝑠HGrpActX/˙
61 eqid G𝑠H=G𝑠H
62 61 subgbas HSubGrpGH=BaseG𝑠H
63 3 62 syl φH=BaseG𝑠H
64 1 subgss HSubGrpGHX
65 3 64 syl φHX
66 2 65 ssfid φHFin
67 63 66 eqeltrrd φBaseG𝑠HFin
68 eqid zX/˙|uBaseG𝑠Hu·˙z=z=zX/˙|uBaseG𝑠Hu·˙z=z
69 eqid xy|xyX/˙gBaseG𝑠Hg·˙x=y=xy|xyX/˙gBaseG𝑠Hg·˙x=y
70 59 60 8 67 30 68 69 sylow2a φPX/˙zX/˙|uBaseG𝑠Hu·˙z=z
71 dvdssub2 PX/˙zX/˙|uBaseG𝑠Hu·˙z=zPX/˙zX/˙|uBaseG𝑠Hu·˙z=zPX/˙PzX/˙|uBaseG𝑠Hu·˙z=z
72 51 52 58 70 71 syl31anc φPX/˙PzX/˙|uBaseG𝑠Hu·˙z=z
73 49 72 mtbid φ¬PzX/˙|uBaseG𝑠Hu·˙z=z
74 hasheq0 zX/˙|uBaseG𝑠Hu·˙z=zFinzX/˙|uBaseG𝑠Hu·˙z=z=0zX/˙|uBaseG𝑠Hu·˙z=z=
75 55 74 syl φzX/˙|uBaseG𝑠Hu·˙z=z=0zX/˙|uBaseG𝑠Hu·˙z=z=
76 dvds0 PP0
77 51 76 syl φP0
78 breq2 zX/˙|uBaseG𝑠Hu·˙z=z=0PzX/˙|uBaseG𝑠Hu·˙z=zP0
79 77 78 syl5ibrcom φzX/˙|uBaseG𝑠Hu·˙z=z=0PzX/˙|uBaseG𝑠Hu·˙z=z
80 75 79 sylbird φzX/˙|uBaseG𝑠Hu·˙z=z=PzX/˙|uBaseG𝑠Hu·˙z=z
81 80 necon3bd φ¬PzX/˙|uBaseG𝑠Hu·˙z=zzX/˙|uBaseG𝑠Hu·˙z=z
82 73 81 mpd φzX/˙|uBaseG𝑠Hu·˙z=z
83 rabn0 zX/˙|uBaseG𝑠Hu·˙z=zzX/˙uBaseG𝑠Hu·˙z=z
84 82 83 sylib φzX/˙uBaseG𝑠Hu·˙z=z
85 63 raleqdv φuHu·˙z=zuBaseG𝑠Hu·˙z=z
86 85 rexbidv φzX/˙uHu·˙z=zzX/˙uBaseG𝑠Hu·˙z=z
87 84 86 mpbird φzX/˙uHu·˙z=z
88 vex zV
89 88 elqs zX/˙gXz=g˙
90 simplrr φgXz=g˙uHu·˙z=zz=g˙
91 90 oveq2d φgXz=g˙uHu·˙z=zu·˙z=u·˙g˙
92 simprr φgXz=g˙uHu·˙z=zu·˙z=z
93 simpll φgXz=g˙uHu·˙z=zφ
94 simprl φgXz=g˙uHu·˙z=zuH
95 simplrl φgXz=g˙uHu·˙z=zgX
96 1 2 3 4 5 6 7 sylow2blem1 φuHgXu·˙g˙=u+˙g˙
97 93 94 95 96 syl3anc φgXz=g˙uHu·˙z=zu·˙g˙=u+˙g˙
98 91 92 97 3eqtr3d φgXz=g˙uHu·˙z=zz=u+˙g˙
99 90 98 eqtr3d φgXz=g˙uHu·˙z=zg˙=u+˙g˙
100 28 ad2antrr φgXz=g˙uHu·˙z=z˙ErX
101 100 95 erth φgXz=g˙uHu·˙z=zg˙u+˙gg˙=u+˙g˙
102 99 101 mpbird φgXz=g˙uHu·˙z=zg˙u+˙g
103 14 ad2antrr φgXz=g˙uHu·˙z=zGGrp
104 39 ad2antrr φgXz=g˙uHu·˙z=zKX
105 eqid invgG=invgG
106 1 105 5 6 eqgval GGrpKXg˙u+˙ggXu+˙gXinvgGg+˙u+˙gK
107 103 104 106 syl2anc φgXz=g˙uHu·˙z=zg˙u+˙ggXu+˙gXinvgGg+˙u+˙gK
108 102 107 mpbid φgXz=g˙uHu·˙z=zgXu+˙gXinvgGg+˙u+˙gK
109 108 simp3d φgXz=g˙uHu·˙z=zinvgGg+˙u+˙gK
110 oveq2 x=invgGg+˙u+˙gg+˙x=g+˙invgGg+˙u+˙g
111 110 oveq1d x=invgGg+˙u+˙gg+˙x-˙g=g+˙invgGg+˙u+˙g-˙g
112 eqid xKg+˙x-˙g=xKg+˙x-˙g
113 ovex g+˙invgGg+˙u+˙g-˙gV
114 111 112 113 fvmpt invgGg+˙u+˙gKxKg+˙x-˙ginvgGg+˙u+˙g=g+˙invgGg+˙u+˙g-˙g
115 109 114 syl φgXz=g˙uHu·˙z=zxKg+˙x-˙ginvgGg+˙u+˙g=g+˙invgGg+˙u+˙g-˙g
116 1 5 34 105 grprinv GGrpgXg+˙invgGg=0G
117 103 95 116 syl2anc φgXz=g˙uHu·˙z=zg+˙invgGg=0G
118 117 oveq1d φgXz=g˙uHu·˙z=zg+˙invgGg+˙u+˙g=0G+˙u+˙g
119 1 105 grpinvcl GGrpgXinvgGgX
120 103 95 119 syl2anc φgXz=g˙uHu·˙z=zinvgGgX
121 65 ad2antrr φgXz=g˙uHu·˙z=zHX
122 121 94 sseldd φgXz=g˙uHu·˙z=zuX
123 1 5 grpcl GGrpuXgXu+˙gX
124 103 122 95 123 syl3anc φgXz=g˙uHu·˙z=zu+˙gX
125 1 5 grpass GGrpgXinvgGgXu+˙gXg+˙invgGg+˙u+˙g=g+˙invgGg+˙u+˙g
126 103 95 120 124 125 syl13anc φgXz=g˙uHu·˙z=zg+˙invgGg+˙u+˙g=g+˙invgGg+˙u+˙g
127 1 5 34 grplid GGrpu+˙gX0G+˙u+˙g=u+˙g
128 103 124 127 syl2anc φgXz=g˙uHu·˙z=z0G+˙u+˙g=u+˙g
129 118 126 128 3eqtr3d φgXz=g˙uHu·˙z=zg+˙invgGg+˙u+˙g=u+˙g
130 129 oveq1d φgXz=g˙uHu·˙z=zg+˙invgGg+˙u+˙g-˙g=u+˙g-˙g
131 1 5 10 grppncan GGrpuXgXu+˙g-˙g=u
132 103 122 95 131 syl3anc φgXz=g˙uHu·˙z=zu+˙g-˙g=u
133 115 130 132 3eqtrd φgXz=g˙uHu·˙z=zxKg+˙x-˙ginvgGg+˙u+˙g=u
134 ovex g+˙x-˙gV
135 134 112 fnmpti xKg+˙x-˙gFnK
136 fnfvelrn xKg+˙x-˙gFnKinvgGg+˙u+˙gKxKg+˙x-˙ginvgGg+˙u+˙granxKg+˙x-˙g
137 135 109 136 sylancr φgXz=g˙uHu·˙z=zxKg+˙x-˙ginvgGg+˙u+˙granxKg+˙x-˙g
138 133 137 eqeltrrd φgXz=g˙uHu·˙z=zuranxKg+˙x-˙g
139 138 expr φgXz=g˙uHu·˙z=zuranxKg+˙x-˙g
140 139 ralimdva φgXz=g˙uHu·˙z=zuHuranxKg+˙x-˙g
141 140 imp φgXz=g˙uHu·˙z=zuHuranxKg+˙x-˙g
142 141 an32s φuHu·˙z=zgXz=g˙uHuranxKg+˙x-˙g
143 dfss3 HranxKg+˙x-˙guHuranxKg+˙x-˙g
144 142 143 sylibr φuHu·˙z=zgXz=g˙HranxKg+˙x-˙g
145 144 expr φuHu·˙z=zgXz=g˙HranxKg+˙x-˙g
146 145 reximdva φuHu·˙z=zgXz=g˙gXHranxKg+˙x-˙g
147 146 ex φuHu·˙z=zgXz=g˙gXHranxKg+˙x-˙g
148 147 com23 φgXz=g˙uHu·˙z=zgXHranxKg+˙x-˙g
149 89 148 syl5bi φzX/˙uHu·˙z=zgXHranxKg+˙x-˙g
150 149 rexlimdv φzX/˙uHu·˙z=zgXHranxKg+˙x-˙g
151 87 150 mpd φgXHranxKg+˙x-˙g