Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylow3lem6 Structured version   Unicode version

Theorem sylow3lem6 16448
 Description: Lemma for sylow3 16449, second part. Using the lemma sylow2a 16435, show that the number of sylow subgroups is equivalent to the number of fixed points under the group action. But is the unique element of the set of Sylow subgroups that is fixed under the group action, so there is exactly one fixed point and so pSyl . (Contributed by Mario Carneiro, 19-Jan-2015.)
Hypotheses
Ref Expression
sylow3.x
sylow3.g
sylow3.xf
sylow3.p
sylow3lem5.a
sylow3lem5.d
sylow3lem5.k pSyl
sylow3lem5.m pSyl
sylow3lem6.n
Assertion
Ref Expression
sylow3lem6 pSyl
Distinct variable groups:   ,,,   ,,,,   ,,,,   ,   ,,,   ,,,,   ,,,,   , ,,   ,,,,
Allowed substitution hints:   ()   ()   (,,)   ()

Proof of Theorem sylow3lem6
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2467 . . . . 5 s s
2 sylow3.x . . . . . 6
3 sylow3.g . . . . . 6
4 sylow3.xf . . . . . 6
5 sylow3.p . . . . . 6
6 sylow3lem5.a . . . . . 6
7 sylow3lem5.d . . . . . 6
8 sylow3lem5.k . . . . . 6 pSyl
9 sylow3lem5.m . . . . . 6 pSyl
102, 3, 4, 5, 6, 7, 8, 9sylow3lem5 16447 . . . . 5 s pSyl
11 eqid 2467 . . . . . . 7 s s
1211slwpgp 16429 . . . . . 6 pSyl pGrp s
138, 12syl 16 . . . . 5 pGrp s
14 slwsubg 16426 . . . . . . . 8 pSyl SubGrp
158, 14syl 16 . . . . . . 7 SubGrp
1611subgbas 16000 . . . . . . 7 SubGrp s
1715, 16syl 16 . . . . . 6 s
182subgss 15997 . . . . . . . 8 SubGrp
1915, 18syl 16 . . . . . . 7
20 ssfi 7737 . . . . . . 7
214, 19, 20syl2anc 661 . . . . . 6
2217, 21eqeltrrd 2556 . . . . 5 s
23 pwfi 7811 . . . . . . 7
244, 23sylib 196 . . . . . 6
25 slwsubg 16426 . . . . . . . . 9 pSyl SubGrp
262subgss 15997 . . . . . . . . 9 SubGrp
2725, 26syl 16 . . . . . . . 8 pSyl
28 selpw 4017 . . . . . . . 8
2927, 28sylibr 212 . . . . . . 7 pSyl
3029ssriv 3508 . . . . . 6 pSyl
31 ssfi 7737 . . . . . 6 pSyl pSyl
3224, 30, 31sylancl 662 . . . . 5 pSyl
33 eqid 2467 . . . . 5 pSyl s pSyl s
34 eqid 2467 . . . . 5 pSyl s pSyl s
351, 10, 13, 22, 32, 33, 34sylow2a 16435 . . . 4 pSyl pSyl s
36 eqcom 2476 . . . . . . . . . . . . . 14
3719adantr 465 . . . . . . . . . . . . . . . 16 pSyl
3837sselda 3504 . . . . . . . . . . . . . . 15 pSyl
3938biantrurd 508 . . . . . . . . . . . . . 14 pSyl
4036, 39syl5bb 257 . . . . . . . . . . . . 13 pSyl
41 simpr 461 . . . . . . . . . . . . . . 15 pSyl
42 simplr 754 . . . . . . . . . . . . . . 15 pSyl pSyl
43 simpr 461 . . . . . . . . . . . . . . . . . 18
44 simpl 457 . . . . . . . . . . . . . . . . . . . 20
4544oveq1d 6297 . . . . . . . . . . . . . . . . . . 19
4645, 44oveq12d 6300 . . . . . . . . . . . . . . . . . 18
4743, 46mpteq12dv 4525 . . . . . . . . . . . . . . . . 17
4847rneqd 5228 . . . . . . . . . . . . . . . 16
49 vex 3116 . . . . . . . . . . . . . . . . . 18
5049mptex 6129 . . . . . . . . . . . . . . . . 17
5150rnex 6715 . . . . . . . . . . . . . . . 16
5248, 9, 51ovmpt2a 6415 . . . . . . . . . . . . . . 15 pSyl
5341, 42, 52syl2anc 661 . . . . . . . . . . . . . 14 pSyl
5453eqeq1d 2469 . . . . . . . . . . . . 13 pSyl
55 slwsubg 16426 . . . . . . . . . . . . . . 15 pSyl SubGrp
5655ad2antlr 726 . . . . . . . . . . . . . 14 pSyl SubGrp
57 eqid 2467 . . . . . . . . . . . . . . 15
58 sylow3lem6.n . . . . . . . . . . . . . . 15
592, 6, 7, 57, 58conjnmzb 16096 . . . . . . . . . . . . . 14 SubGrp
6056, 59syl 16 . . . . . . . . . . . . 13 pSyl
6140, 54, 603bitr4d 285 . . . . . . . . . . . 12 pSyl
6261ralbidva 2900 . . . . . . . . . . 11 pSyl
63 dfss3 3494 . . . . . . . . . . 11
6462, 63syl6bbr 263 . . . . . . . . . 10 pSyl
6517adantr 465 . . . . . . . . . . 11 pSyl s
6665raleqdv 3064 . . . . . . . . . 10 pSyl s
67 eqid 2467 . . . . . . . . . . . . 13 s s
683ad2antrr 725 . . . . . . . . . . . . . . . 16 pSyl
6958, 2, 6nmzsubg 16037 . . . . . . . . . . . . . . . 16 SubGrp
7068, 69syl 16 . . . . . . . . . . . . . . 15 pSyl SubGrp
71 eqid 2467 . . . . . . . . . . . . . . . 16 s s
7271subgbas 16000 . . . . . . . . . . . . . . 15 SubGrp s
7370, 72syl 16 . . . . . . . . . . . . . 14 pSyl s
744ad2antrr 725 . . . . . . . . . . . . . . 15 pSyl
752subgss 15997 . . . . . . . . . . . . . . . 16 SubGrp
7670, 75syl 16 . . . . . . . . . . . . . . 15 pSyl
77 ssfi 7737 . . . . . . . . . . . . . . 15
7874, 76, 77syl2anc 661 . . . . . . . . . . . . . 14 pSyl
7973, 78eqeltrrd 2556 . . . . . . . . . . . . 13 pSyl s
808ad2antrr 725 . . . . . . . . . . . . . 14 pSyl pSyl
81 simpr 461 . . . . . . . . . . . . . 14 pSyl
8271subgslw 16432 . . . . . . . . . . . . . 14 SubGrp pSyl pSyl s
8370, 80, 81, 82syl3anc 1228 . . . . . . . . . . . . 13 pSyl pSyl s
84 simplr 754 . . . . . . . . . . . . . 14 pSyl pSyl
8555ad2antlr 726 . . . . . . . . . . . . . . 15 pSyl SubGrp
8658, 2, 6ssnmz 16038 . . . . . . . . . . . . . . 15 SubGrp
8785, 86syl 16 . . . . . . . . . . . . . 14 pSyl
8871subgslw 16432 . . . . . . . . . . . . . 14 SubGrp pSyl pSyl s
8970, 84, 87, 88syl3anc 1228 . . . . . . . . . . . . 13 pSyl pSyl s
90 fvex 5874 . . . . . . . . . . . . . . . . 17
912, 90eqeltri 2551 . . . . . . . . . . . . . . . 16
9291rabex 4598 . . . . . . . . . . . . . . 15
9358, 92eqeltri 2551 . . . . . . . . . . . . . 14
9471, 6ressplusg 14593 . . . . . . . . . . . . . 14 s
9593, 94ax-mp 5 . . . . . . . . . . . . 13 s
96 eqid 2467 . . . . . . . . . . . . 13 s s
9767, 79, 83, 89, 95, 96sylow2 16442 . . . . . . . . . . . 12 pSyl s s
9858, 2, 6, 71nmznsg 16040 . . . . . . . . . . . . . . . 16 SubGrp NrmSGrps
9985, 98syl 16 . . . . . . . . . . . . . . 15 pSyl NrmSGrps
100 eqid 2467 . . . . . . . . . . . . . . . 16 s s
10167, 95, 96, 100conjnsg 16097 . . . . . . . . . . . . . . 15 NrmSGrps s s
10299, 101sylan 471 . . . . . . . . . . . . . 14 pSyl s s
103 eqeq2 2482 . . . . . . . . . . . . . 14 s s
104102, 103syl5ibrcom 222 . . . . . . . . . . . . 13 pSyl s s
105104rexlimdva 2955 . . . . . . . . . . . 12 pSyl s s
10697, 105mpd 15 . . . . . . . . . . 11 pSyl
107 simpr 461 . . . . . . . . . . . 12 pSyl
10815ad2antrr 725 . . . . . . . . . . . . . 14 pSyl SubGrp
109107, 108eqeltrd 2555 . . . . . . . . . . . . 13 pSyl SubGrp
110109, 86syl 16 . . . . . . . . . . . 12 pSyl
111107, 110eqsstr3d 3539 . . . . . . . . . . 11 pSyl
112106, 111impbida 830 . . . . . . . . . 10 pSyl
11364, 66, 1123bitr3d 283 . . . . . . . . 9 pSyl s
114113rabbidva 3104 . . . . . . . 8 pSyl s pSyl
115 rabsn 4094 . . . . . . . . 9 pSyl pSyl
1168, 115syl 16 . . . . . . . 8 pSyl
117114, 116eqtrd 2508 . . . . . . 7 pSyl s
118117fveq2d 5868 . . . . . 6 pSyl s
119 hashsng 12402 . . . . . . 7 pSyl
1208, 119syl 16 . . . . . 6
121118, 120eqtrd 2508 . . . . 5 pSyl s
122121oveq2d 6298 . . . 4 pSyl pSyl s pSyl
12335, 122breqtrd 4471 . . 3 pSyl
124 prmnn 14075 . . . . 5
1255, 124syl 16 . . . 4
126 hashcl 12392 . . . . . 6 pSyl pSyl
12732, 126syl 16 . . . . 5 pSyl
128127nn0zd 10960 . . . 4 pSyl
129 1zzd 10891 . . . 4
130 moddvds 13850 . . . 4 pSyl pSyl pSyl
131125, 128, 129, 130syl3anc 1228 . . 3 pSyl pSyl
132123, 131mpbird 232 . 2 pSyl
133 prmuz2 14090 . . 3
134 eluz2b2 11150 . . . 4
135 nnre 10539 . . . . 5
136 1mod 11992 . . . . 5
137135, 136sylan 471 . . . 4
138134, 137sylbi 195 . . 3
1395, 133, 1383syl 20 . 2
140132, 139eqtrd 2508 1 pSyl
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 184   wa 369   wceq 1379   wcel 1767  wral 2814  wrex 2815  crab 2818  cvv 3113   wss 3476  cpw 4010  csn 4027  cpr 4029   class class class wbr 4447  copab 4504   cmpt 4505   crn 5000  cfv 5586  (class class class)co 6282   cmpt2 6284  cfn 7513  cr 9487  c1 9489   clt 9624   cmin 9801  cn 10532  c2 10581  cn0 10791  cz 10860  cuz 11078   cmo 11960  chash 12369   cdivides 13843  cprime 14072  cbs 14486   ↾s cress 14487   cplusg 14551  cgrp 15723  csg 15726  SubGrpcsubg 15990  NrmSGrpcnsg 15991   pGrp cpgp 16347   pSyl cslw 16348 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574  ax-inf2 8054  ax-cnex 9544  ax-resscn 9545  ax-1cn 9546  ax-icn 9547  ax-addcl 9548  ax-addrcl 9549  ax-mulcl 9550  ax-mulrcl 9551  ax-mulcom 9552  ax-addass 9553  ax-mulass 9554  ax-distr 9555  ax-i2m1 9556  ax-1ne0 9557  ax-1rid 9558  ax-rnegex 9559  ax-rrecex 9560  ax-cnre 9561  ax-pre-lttri 9562  ax-pre-lttrn 9563  ax-pre-ltadd 9564  ax-pre-mulgt0 9565  ax-pre-sup 9566 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-fal 1385  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-disj 4418  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-se 4839  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-isom 5595  df-riota 6243  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-2o 7128  df-oadd 7131  df-omul 7132  df-er 7308  df-ec 7310  df-qs 7314  df-map 7419  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-sup 7897  df-oi 7931  df-card 8316  df-acn 8319  df-cda 8544  df-pnf 9626  df-mnf 9627  df-xr 9628  df-ltxr 9629  df-le 9630  df-sub 9803  df-neg 9804  df-div 10203  df-nn 10533  df-2 10590  df-3 10591  df-n0 10792  df-z 10861  df-uz 11079  df-q 11179  df-rp 11217  df-fz 11669  df-fzo 11789  df-fl 11893  df-mod 11961  df-seq 12072  df-exp 12131  df-fac 12318  df-bc 12345  df-hash 12370  df-cj 12891  df-re 12892  df-im 12893  df-sqrt 13027  df-abs 13028  df-clim 13270  df-sum 13468  df-dvds 13844  df-gcd 14000  df-prm 14073  df-pc 14216  df-ndx 14489  df-slot 14490  df-base 14491  df-sets 14492  df-ress 14493  df-plusg 14564  df-0g 14693  df-mnd 15728  df-submnd 15778  df-grp 15858  df-minusg 15859  df-sbg 15860  df-mulg 15861  df-subg 15993  df-nsg 15994  df-eqg 15995  df-ghm 16060  df-ga 16123  df-od 16349  df-pgp 16351  df-slw 16352 This theorem is referenced by:  sylow3  16449
 Copyright terms: Public domain W3C validator