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

Theorem ablfac2 15637
 Description: Choose generators for each cyclic group in ablfac 15636. (Contributed by Mario Carneiro, 28-Apr-2016.)
Hypotheses
Ref Expression
ablfac.b
ablfac.c SubGrp s CycGrp pGrp
ablfac.1
ablfac.2
ablfac2.m .g
ablfac2.s
Assertion
Ref Expression
ablfac2 Word DProd DProd
Distinct variable groups:   ,   ,,,,   ,,   ,,,   ,,,   ,,,,
Allowed substitution hints:   ()   ()   (,,)   (,)

Proof of Theorem ablfac2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ablfac.b . . 3
2 ablfac.c . . 3 SubGrp s CycGrp pGrp
3 ablfac.1 . . 3
4 ablfac.2 . . 3
51, 2, 3, 4ablfac 15636 . 2 Word DProd DProd
6 wrdf 11723 . . . . . . . . . 10 Word ..^
76ad2antlr 708 . . . . . . . . 9 Word DProd DProd ..^
8 fdm 5587 . . . . . . . . 9 ..^ ..^
97, 8syl 16 . . . . . . . 8 Word DProd DProd ..^
10 fzofi 11303 . . . . . . . 8 ..^
119, 10syl6eqel 2523 . . . . . . 7 Word DProd DProd
129feq2d 5573 . . . . . . . . . . . . 13 Word DProd DProd ..^
137, 12mpbird 224 . . . . . . . . . . . 12 Word DProd DProd
1413ffvelrnda 5862 . . . . . . . . . . 11 Word DProd DProd
15 oveq2 6081 . . . . . . . . . . . . . 14 s s
1615eleq1d 2501 . . . . . . . . . . . . 13 s CycGrp pGrp s CycGrp pGrp
1716, 2elrab2 3086 . . . . . . . . . . . 12 SubGrp s CycGrp pGrp
1817simplbi 447 . . . . . . . . . . 11 SubGrp
1914, 18syl 16 . . . . . . . . . 10 Word DProd DProd SubGrp
201subgss 14935 . . . . . . . . . 10 SubGrp
2119, 20syl 16 . . . . . . . . 9 Word DProd DProd
22 inss1 3553 . . . . . . . . . . . . 13 CycGrp pGrp CycGrp
2317simprbi 451 . . . . . . . . . . . . . 14 s CycGrp pGrp
2414, 23syl 16 . . . . . . . . . . . . 13 Word DProd DProd s CycGrp pGrp
2522, 24sseldi 3338 . . . . . . . . . . . 12 Word DProd DProd s CycGrp
26 eqid 2435 . . . . . . . . . . . . . 14 s s
27 eqid 2435 . . . . . . . . . . . . . 14 .gs .gs
2826, 27iscyg 15479 . . . . . . . . . . . . 13 s CycGrp s s .gs s
2928simprbi 451 . . . . . . . . . . . 12 s CycGrp s .gs s
3025, 29syl 16 . . . . . . . . . . 11 Word DProd DProd s .gs s
31 eqid 2435 . . . . . . . . . . . . . 14 s s
3231subgbas 14938 . . . . . . . . . . . . 13 SubGrp s
3319, 32syl 16 . . . . . . . . . . . 12 Word DProd DProd s
3433rexeqdv 2903 . . . . . . . . . . 11 Word DProd DProd .gs s s .gs s
3530, 34mpbird 224 . . . . . . . . . 10 Word DProd DProd .gs s
3619ad2antrr 707 . . . . . . . . . . . . . . 15 Word DProd DProd SubGrp
37 simpr 448 . . . . . . . . . . . . . . 15 Word DProd DProd
38 simplr 732 . . . . . . . . . . . . . . 15 Word DProd DProd
39 ablfac2.m . . . . . . . . . . . . . . . 16 .g
4039, 31, 27subgmulg 14948 . . . . . . . . . . . . . . 15 SubGrp .gs
4136, 37, 38, 40syl3anc 1184 . . . . . . . . . . . . . 14 Word DProd DProd .gs
4241mpteq2dva 4287 . . . . . . . . . . . . 13 Word DProd DProd .gs
4342rneqd 5089 . . . . . . . . . . . 12 Word DProd DProd .gs
4433adantr 452 . . . . . . . . . . . 12 Word DProd DProd s
4543, 44eqeq12d 2449 . . . . . . . . . . 11 Word DProd DProd .gs s
4645rexbidva 2714 . . . . . . . . . 10 Word DProd DProd .gs s
4735, 46mpbird 224 . . . . . . . . 9 Word DProd DProd
48 ssrexv 3400 . . . . . . . . 9
4921, 47, 48sylc 58 . . . . . . . 8 Word DProd DProd
5049ralrimiva 2781 . . . . . . 7 Word DProd DProd
51 oveq2 6081 . . . . . . . . . . 11
5251mpteq2dv 4288 . . . . . . . . . 10
5352rneqd 5089 . . . . . . . . 9
5453eqeq1d 2443 . . . . . . . 8
5554ac6sfi 7343 . . . . . . 7
5611, 50, 55syl2anc 643 . . . . . 6 Word DProd DProd
57 simprl 733 . . . . . . . . . . 11 Word DProd DProd
589adantr 452 . . . . . . . . . . . 12 Word DProd DProd ..^
5958feq2d 5573 . . . . . . . . . . 11 Word DProd DProd ..^
6057, 59mpbid 202 . . . . . . . . . 10 Word DProd DProd ..^
61 iswrdi 11721 . . . . . . . . . 10 ..^ Word
6260, 61syl 16 . . . . . . . . 9 Word DProd DProd Word
63 fdm 5587 . . . . . . . . . . . . . . . 16 ..^ ..^
6460, 63syl 16 . . . . . . . . . . . . . . 15 Word DProd DProd ..^
6564, 58eqtr4d 2470 . . . . . . . . . . . . . 14 Word DProd DProd
6665eleq2d 2502 . . . . . . . . . . . . 13 Word DProd DProd
6766biimpa 471 . . . . . . . . . . . 12 Word DProd DProd
68 simprr 734 . . . . . . . . . . . . . 14 Word DProd DProd
69 simpl 444 . . . . . . . . . . . . . . . . . . . 20
7069fveq2d 5724 . . . . . . . . . . . . . . . . . . 19
7170oveq2d 6089 . . . . . . . . . . . . . . . . . 18
7271mpteq2dva 4287 . . . . . . . . . . . . . . . . 17
7372rneqd 5089 . . . . . . . . . . . . . . . 16
74 fveq2 5720 . . . . . . . . . . . . . . . 16
7573, 74eqeq12d 2449 . . . . . . . . . . . . . . 15
7675rspccva 3043 . . . . . . . . . . . . . 14
7768, 76sylan 458 . . . . . . . . . . . . 13 Word DProd DProd
7813adantr 452 . . . . . . . . . . . . . 14 Word DProd DProd
7978ffvelrnda 5862 . . . . . . . . . . . . 13 Word DProd DProd
8077, 79eqeltrd 2509 . . . . . . . . . . . 12 Word DProd DProd
8167, 80syldan 457 . . . . . . . . . . 11 Word DProd DProd
82 ablfac2.s . . . . . . . . . . . 12
83 fveq2 5720 . . . . . . . . . . . . . . . 16
8483oveq2d 6089 . . . . . . . . . . . . . . 15
8584mpteq2dv 4288 . . . . . . . . . . . . . 14
8685rneqd 5089 . . . . . . . . . . . . 13
8786cbvmptv 4292 . . . . . . . . . . . 12
8882, 87eqtri 2455 . . . . . . . . . . 11
8981, 88fmptd 5885 . . . . . . . . . 10 Word DProd DProd
90 simprl 733 . . . . . . . . . . . 12 Word DProd DProd DProd
9190adantr 452 . . . . . . . . . . 11 Word DProd DProd DProd
9265raleqdv 2902 . . . . . . . . . . . . . . 15 Word DProd DProd
9368, 92mpbird 224 . . . . . . . . . . . . . 14 Word DProd DProd
94 mpteq12 4280 . . . . . . . . . . . . . 14
9565, 93, 94syl2anc 643 . . . . . . . . . . . . 13 Word DProd DProd
9682, 95syl5eq 2479 . . . . . . . . . . . 12 Word DProd DProd
97 dprdf 15554 . . . . . . . . . . . . . 14 DProd SubGrp
9891, 97syl 16 . . . . . . . . . . . . 13 Word DProd DProd SubGrp
9998feqmptd 5771 . . . . . . . . . . . 12 Word DProd DProd
10096, 99eqtr4d 2470 . . . . . . . . . . 11 Word DProd DProd
10191, 100breqtrrd 4230 . . . . . . . . . 10 Word DProd DProd DProd
102100oveq2d 6089 . . . . . . . . . . 11 Word DProd DProd DProd DProd
103 simplrr 738 . . . . . . . . . . 11 Word DProd DProd DProd
104102, 103eqtrd 2467 . . . . . . . . . 10 Word DProd DProd DProd
10589, 101, 1043jca 1134 . . . . . . . . 9 Word DProd DProd DProd DProd
10662, 105jca 519 . . . . . . . 8 Word DProd DProd Word DProd DProd
107106ex 424 . . . . . . 7 Word DProd DProd Word DProd DProd
108107eximdv 1632 . . . . . 6 Word DProd DProd Word DProd DProd
10956, 108mpd 15 . . . . 5 Word DProd DProd Word DProd DProd
110 df-rex 2703 . . . . 5 Word DProd DProd Word DProd DProd
111109, 110sylibr 204 . . . 4 Word DProd DProd Word DProd DProd
112111ex 424 . . 3 Word DProd DProd Word DProd DProd
113112rexlimdva 2822 . 2 Word DProd DProd Word DProd DProd
1145, 113mpd 15 1 Word DProd DProd
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   w3a 936  wex 1550   wceq 1652   wcel 1725  wral 2697  wrex 2698  crab 2701   cin 3311   wss 3312   class class class wbr 4204   cmpt 4258   cdm 4870   crn 4871  wf 5442  cfv 5446  (class class class)co 6073  cfn 7101  cc0 8980  cz 10272  ..^cfzo 11125  chash 11608  Word cword 11707  cbs 13459   ↾s cress 13460  cgrp 14675  .gcmg 14679  SubGrpcsubg 14928   pGrp cpgp 15155  cabel 15403  CycGrpccyg 15477   DProd cdprd 15544 This theorem is referenced by:  dchrpt  21041 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-inf2 7586  ax-cnex 9036  ax-resscn 9037  ax-1cn 9038  ax-icn 9039  ax-addcl 9040  ax-addrcl 9041  ax-mulcl 9042  ax-mulrcl 9043  ax-mulcom 9044  ax-addass 9045  ax-mulass 9046  ax-distr 9047  ax-i2m1 9048  ax-1ne0 9049  ax-1rid 9050  ax-rnegex 9051  ax-rrecex 9052  ax-cnre 9053  ax-pre-lttri 9054  ax-pre-lttrn 9055  ax-pre-ltadd 9056  ax-pre-mulgt0 9057  ax-pre-sup 9058 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-int 4043  df-iun 4087  df-iin 4088  df-disj 4175  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-se 4534  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-isom 5455  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-of 6297  df-1st 6341  df-2nd 6342  df-tpos 6471  df-rpss 6514  df-riota 6541  df-recs 6625  df-rdg 6660  df-1o 6716  df-2o 6717  df-oadd 6720  df-omul 6721  df-er 6897  df-ec 6899  df-qs 6903  df-map 7012  df-pm 7013  df-ixp 7056  df-en 7102  df-dom 7103  df-sdom 7104  df-fin 7105  df-sup 7438  df-oi 7469  df-card 7816  df-acn 7819  df-cda 8038  df-pnf 9112  df-mnf 9113  df-xr 9114  df-ltxr 9115  df-le 9116  df-sub 9283  df-neg 9284  df-div 9668  df-nn 9991  df-2 10048  df-3 10049  df-n0 10212  df-z 10273  df-uz 10479  df-q 10565  df-rp 10603  df-fz 11034  df-fzo 11126  df-fl 11192  df-mod 11241  df-seq 11314  df-exp 11373  df-fac 11557  df-bc 11584  df-hash 11609  df-word 11713  df-concat 11714  df-s1 11715  df-cj 11894  df-re 11895  df-im 11896  df-sqr 12030  df-abs 12031  df-clim 12272  df-sum 12470  df-dvds 12843  df-gcd 12997  df-prm 13070  df-pc 13201  df-ndx 13462  df-slot 13463  df-base 13464  df-sets 13465  df-ress 13466  df-plusg 13532  df-0g 13717  df-gsum 13718  df-mre 13801  df-mrc 13802  df-acs 13804  df-mnd 14680  df-mhm 14728  df-submnd 14729  df-grp 14802  df-minusg 14803  df-sbg 14804  df-mulg 14805  df-subg 14931  df-eqg 14933  df-ghm 14994  df-gim 15036  df-ga 15057  df-cntz 15106  df-oppg 15132  df-od 15157  df-gex 15158  df-pgp 15159  df-lsm 15260  df-pj1 15261  df-cmn 15404  df-abl 15405  df-cyg 15478  df-dprd 15546
 Copyright terms: Public domain W3C validator