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

Theorem sylow3lem1 14987
 Description: Lemma for sylow3 14993, first part. (Contributed by Mario Carneiro, 19-Jan-2015.)
Hypotheses
Ref Expression
sylow3.x
sylow3.g
sylow3.xf
sylow3.p
sylow3lem1.a
sylow3lem1.d
sylow3lem1.m pSyl
Assertion
Ref Expression
sylow3lem1 pSyl
Distinct variable groups:   ,,,   , ,,   ,,,   ,,,   ,,,   , ,,   ,,,

Proof of Theorem sylow3lem1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sylow3.g . . 3
2 ovex 5925 . . 3 pSyl
31, 2jctir 524 . 2 pSyl
4 sylow3.xf . . . . . . . . . . 11
5 sylow3.p . . . . . . . . . . 11
6 sylow3.x . . . . . . . . . . . 12
76fislw 14985 . . . . . . . . . . 11 pSyl SubGrp
81, 4, 5, 7syl3anc 1182 . . . . . . . . . 10 pSyl SubGrp
98biimpa 470 . . . . . . . . 9 pSyl SubGrp
109adantrl 696 . . . . . . . 8 pSyl SubGrp
1110simpld 445 . . . . . . 7 pSyl SubGrp
12 simprl 732 . . . . . . 7 pSyl
13 sylow3lem1.a . . . . . . . 8
14 sylow3lem1.d . . . . . . . 8
15 eqid 2316 . . . . . . . 8
166, 13, 14, 15conjsubg 14763 . . . . . . 7 SubGrp SubGrp
1711, 12, 16syl2anc 642 . . . . . 6 pSyl SubGrp
186, 13, 14, 15conjsubgen 14764 . . . . . . . . 9 SubGrp
1911, 12, 18syl2anc 642 . . . . . . . 8 pSyl
204adantr 451 . . . . . . . . . 10 pSyl
216subgss 14671 . . . . . . . . . . 11 SubGrp
2211, 21syl 15 . . . . . . . . . 10 pSyl
23 ssfi 7126 . . . . . . . . . 10
2420, 22, 23syl2anc 642 . . . . . . . . 9 pSyl
256subgss 14671 . . . . . . . . . . 11 SubGrp
2617, 25syl 15 . . . . . . . . . 10 pSyl
27 ssfi 7126 . . . . . . . . . 10
2820, 26, 27syl2anc 642 . . . . . . . . 9 pSyl
29 hashen 11393 . . . . . . . . 9
3024, 28, 29syl2anc 642 . . . . . . . 8 pSyl
3119, 30mpbird 223 . . . . . . 7 pSyl
3210simprd 449 . . . . . . 7 pSyl
3331, 32eqtr3d 2350 . . . . . 6 pSyl
346fislw 14985 . . . . . . . 8 pSyl SubGrp
351, 4, 5, 34syl3anc 1182 . . . . . . 7 pSyl SubGrp
3635adantr 451 . . . . . 6 pSyl pSyl SubGrp
3717, 33, 36mpbir2and 888 . . . . 5 pSyl pSyl
3837ralrimivva 2669 . . . 4 pSyl pSyl
39 sylow3lem1.m . . . . 5 pSyl
4039fmpt2 6233 . . . 4 pSyl pSyl pSyl pSyl
4138, 40sylib 188 . . 3 pSyl pSyl
421adantr 451 . . . . . . . 8 pSyl
43 eqid 2316 . . . . . . . . 9
446, 43grpidcl 14559 . . . . . . . 8
4542, 44syl 15 . . . . . . 7 pSyl
46 simpr 447 . . . . . . 7 pSyl pSyl
47 simpr 447 . . . . . . . . . 10
48 simpl 443 . . . . . . . . . . . 12
4948oveq1d 5915 . . . . . . . . . . 11
5049, 48oveq12d 5918 . . . . . . . . . 10
5147, 50mpteq12dv 4135 . . . . . . . . 9
5251rneqd 4943 . . . . . . . 8
53 vex 2825 . . . . . . . . . 10
5453mptex 5787 . . . . . . . . 9
5554rnex 4979 . . . . . . . 8
5652, 39, 55ovmpt2a 6020 . . . . . . 7 pSyl
5745, 46, 56syl2anc 642 . . . . . 6 pSyl
581ad2antrr 706 . . . . . . . . . . . . 13 pSyl
59 slwsubg 14970 . . . . . . . . . . . . . . . 16 pSyl SubGrp
6059adantl 452 . . . . . . . . . . . . . . 15 pSyl SubGrp
616subgss 14671 . . . . . . . . . . . . . . 15 SubGrp
6260, 61syl 15 . . . . . . . . . . . . . 14 pSyl
6362sselda 3214 . . . . . . . . . . . . 13 pSyl
646, 13, 43grplid 14561 . . . . . . . . . . . . 13
6558, 63, 64syl2anc 642 . . . . . . . . . . . 12 pSyl
6665oveq1d 5915 . . . . . . . . . . 11 pSyl
676, 43, 14grpsubid1 14600 . . . . . . . . . . . 12
6858, 63, 67syl2anc 642 . . . . . . . . . . 11 pSyl
6966, 68eqtrd 2348 . . . . . . . . . 10 pSyl
7069mpteq2dva 4143 . . . . . . . . 9 pSyl
71 mptresid 5041 . . . . . . . . 9
7270, 71syl6eq 2364 . . . . . . . 8 pSyl
7372rneqd 4943 . . . . . . 7 pSyl
74 rnresi 5065 . . . . . . 7
7573, 74syl6eq 2364 . . . . . 6 pSyl
7657, 75eqtrd 2348 . . . . 5 pSyl
77 ovex 5925 . . . . . . . . . 10
78 oveq2 5908 . . . . . . . . . . 11
7978oveq1d 5915 . . . . . . . . . 10
8077, 79abrexco 5807 . . . . . . . . 9
81 simprr 733 . . . . . . . . . . . . 13 pSyl
82 simplr 731 . . . . . . . . . . . . 13 pSyl pSyl
83 simpr 447 . . . . . . . . . . . . . . . 16
84 simpl 443 . . . . . . . . . . . . . . . . . 18
8584oveq1d 5915 . . . . . . . . . . . . . . . . 17
8685, 84oveq12d 5918 . . . . . . . . . . . . . . . 16
8783, 86mpteq12dv 4135 . . . . . . . . . . . . . . 15
8887rneqd 4943 . . . . . . . . . . . . . 14
8953mptex 5787 . . . . . . . . . . . . . . 15
9089rnex 4979 . . . . . . . . . . . . . 14
9188, 39, 90ovmpt2a 6020 . . . . . . . . . . . . 13 pSyl
9281, 82, 91syl2anc 642 . . . . . . . . . . . 12 pSyl
93 eqid 2316 . . . . . . . . . . . . 13
9493rnmpt 4962 . . . . . . . . . . . 12
9592, 94syl6eq 2364 . . . . . . . . . . 11 pSyl
9695rexeqdv 2777 . . . . . . . . . 10 pSyl
9796abbidv 2430 . . . . . . . . 9 pSyl
9842adantr 451 . . . . . . . . . . . . . . 15 pSyl
9998adantr 451 . . . . . . . . . . . . . 14 pSyl
100 simprl 732 . . . . . . . . . . . . . . . . 17 pSyl
1016, 13grpcl 14544 . . . . . . . . . . . . . . . . 17
10298, 100, 81, 101syl3anc 1182 . . . . . . . . . . . . . . . 16 pSyl
103102adantr 451 . . . . . . . . . . . . . . 15 pSyl
10463adantlr 695 . . . . . . . . . . . . . . 15 pSyl
1056, 13grpcl 14544 . . . . . . . . . . . . . . 15
10699, 103, 104, 105syl3anc 1182 . . . . . . . . . . . . . 14 pSyl
10781adantr 451 . . . . . . . . . . . . . 14 pSyl
108100adantr 451 . . . . . . . . . . . . . 14 pSyl
1096, 13, 14grpsubsub4 14607 . . . . . . . . . . . . . 14
11099, 106, 107, 108, 109syl13anc 1184 . . . . . . . . . . . . 13 pSyl
1116, 13grpass 14545 . . . . . . . . . . . . . . . . 17
11299, 108, 107, 104, 111syl13anc 1184 . . . . . . . . . . . . . . . 16 pSyl
113112oveq1d 5915 . . . . . . . . . . . . . . 15 pSyl
1146, 13grpcl 14544 . . . . . . . . . . . . . . . . 17
11599, 107, 104, 114syl3anc 1182 . . . . . . . . . . . . . . . 16 pSyl
1166, 13, 14grpaddsubass 14604 . . . . . . . . . . . . . . . 16
11799, 108, 115, 107, 116syl13anc 1184 . . . . . . . . . . . . . . 15 pSyl
118113, 117eqtrd 2348 . . . . . . . . . . . . . 14 pSyl
119118oveq1d 5915 . . . . . . . . . . . . 13 pSyl
120110, 119eqtr3d 2350 . . . . . . . . . . . 12 pSyl
121120eqeq2d 2327 . . . . . . . . . . 11 pSyl
122121rexbidva 2594 . . . . . . . . . 10 pSyl
123122abbidv 2430 . . . . . . . . 9 pSyl
12480, 97, 1233eqtr4a 2374 . . . . . . . 8 pSyl
125 eqid 2316 . . . . . . . . 9
126125rnmpt 4962 . . . . . . . 8
127 eqid 2316 . . . . . . . . 9
128127rnmpt 4962 . . . . . . . 8
129124, 126, 1283eqtr4g 2373 . . . . . . 7 pSyl
13041ad2antrr 706 . . . . . . . . 9 pSyl pSyl pSyl
131 fovrn 6032 . . . . . . . . 9 pSyl pSyl pSyl pSyl
132130, 81, 82, 131syl3anc 1182 . . . . . . . 8 pSyl pSyl
133 simpr 447 . . . . . . . . . . . 12
134 simpl 443 . . . . . . . . . . . . . 14
135134oveq1d 5915 . . . . . . . . . . . . 13
136135, 134oveq12d 5918 . . . . . . . . . . . 12
137133, 136mpteq12dv 4135 . . . . . . . . . . 11
138 oveq2 5908 . . . . . . . . . . . . 13
139138oveq1d 5915 . . . . . . . . . . . 12
140139cbvmptv 4148 . . . . . . . . . . 11
141137, 140syl6eq 2364 . . . . . . . . . 10
142141rneqd 4943 . . . . . . . . 9
143 ovex 5925 . . . . . . . . . . 11
144143mptex 5787 . . . . . . . . . 10
145144rnex 4979 . . . . . . . . 9
146142, 39, 145ovmpt2a 6020 . . . . . . . 8 pSyl
147100, 132, 146syl2anc 642 . . . . . . 7 pSyl
148 simpr 447 . . . . . . . . . . 11
149 simpl 443 . . . . . . . . . . . . 13
150149oveq1d 5915 . . . . . . . . . . . 12
151150, 149oveq12d 5918 . . . . . . . . . . 11
152148, 151mpteq12dv 4135 . . . . . . . . . 10
153152rneqd 4943 . . . . . . . . 9
15453mptex 5787 . . . . . . . . . 10
155154rnex 4979 . . . . . . . . 9
156153, 39, 155ovmpt2a 6020 . . . . . . . 8 pSyl
157102, 82, 156syl2anc 642 . . . . . . 7 pSyl
158129, 147, 1573eqtr4rd 2359 . . . . . 6 pSyl
159158ralrimivva 2669 . . . . 5 pSyl
16076, 159jca 518 . . . 4 pSyl
161160ralrimiva 2660 . . 3 pSyl
16241, 161jca 518 . 2 pSyl pSyl pSyl
1636, 13, 43isga 14794 . 2 pSyl pSyl pSyl pSyl pSyl
1643, 162, 163sylanbrc 645 1 pSyl
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   wceq 1633   wcel 1701  cab 2302  wral 2577  wrex 2578  cvv 2822   wss 3186   class class class wbr 4060   cmpt 4114   cid 4341   cxp 4724   crn 4727   cres 4728  wf 5288  cfv 5292  (class class class)co 5900   cmpt2 5902   cen 6903  cfn 6906  cexp 11151  chash 11384  cprime 12805   cpc 12936  cbs 13195   cplusg 13255  c0g 13449  cgrp 14411  csg 14414  SubGrpcsubg 14664   cga 14792   pSyl cslw 14892 This theorem is referenced by:  sylow3lem3  14989  sylow3lem5  14991 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-13 1703  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-rep 4168  ax-sep 4178  ax-nul 4186  ax-pow 4225  ax-pr 4251  ax-un 4549  ax-inf2 7387  ax-cnex 8838  ax-resscn 8839  ax-1cn 8840  ax-icn 8841  ax-addcl 8842  ax-addrcl 8843  ax-mulcl 8844  ax-mulrcl 8845  ax-mulcom 8846  ax-addass 8847  ax-mulass 8848  ax-distr 8849  ax-i2m1 8850  ax-1ne0 8851  ax-1rid 8852  ax-rnegex 8853  ax-rrecex 8854  ax-cnre 8855  ax-pre-lttri 8856  ax-pre-lttrn 8857  ax-pre-ltadd 8858  ax-pre-mulgt0 8859  ax-pre-sup 8860 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-nel 2482  df-ral 2582  df-rex 2583  df-reu 2584  df-rmo 2585  df-rab 2586  df-v 2824  df-sbc 3026  df-csb 3116  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-pss 3202  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-tp 3682  df-op 3683  df-uni 3865  df-int 3900  df-iun 3944  df-disj 4031  df-br 4061  df-opab 4115  df-mpt 4116  df-tr 4151  df-eprel 4342  df-id 4346  df-po 4351  df-so 4352  df-fr 4389  df-se 4390  df-we 4391  df-ord 4432  df-on 4433  df-lim 4434  df-suc 4435  df-om 4694  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-iota 5256  df-fun 5294  df-fn 5295  df-f 5296  df-f1 5297  df-fo 5298  df-f1o 5299  df-fv 5300  df-isom 5301  df-ov 5903  df-oprab 5904  df-mpt2 5905  df-1st 6164  df-2nd 6165  df-riota 6346  df-recs 6430  df-rdg 6465  df-1o 6521  df-2o 6522  df-oadd 6525  df-omul 6526  df-er 6702  df-ec 6704  df-qs 6708  df-map 6817  df-en 6907  df-dom 6908  df-sdom 6909  df-fin 6910  df-sup 7239  df-oi 7270  df-card 7617  df-acn 7620  df-cda 7839  df-pnf 8914  df-mnf 8915  df-xr 8916  df-ltxr 8917  df-le 8918  df-sub 9084  df-neg 9085  df-div 9469  df-nn 9792  df-2 9849  df-3 9850  df-n0 10013  df-z 10072  df-uz 10278  df-q 10364  df-rp 10402  df-fz 10830  df-fzo 10918  df-fl 10972  df-mod 11021  df-seq 11094  df-exp 11152  df-fac 11336  df-bc 11363  df-hash 11385  df-cj 11631  df-re 11632  df-im 11633  df-sqr 11767  df-abs 11768  df-clim 12009  df-sum 12206  df-dvds 12579  df-gcd 12733  df-prm 12806  df-pc 12937  df-ndx 13198  df-slot 13199  df-base 13200  df-sets 13201  df-ress 13202  df-plusg 13268  df-0g 13453  df-mnd 14416  df-submnd 14465  df-grp 14538  df-minusg 14539  df-sbg 14540  df-mulg 14541  df-subg 14667  df-eqg 14669  df-ghm 14730  df-ga 14793  df-od 14893  df-pgp 14895  df-slw 14896
 Copyright terms: Public domain W3C validator