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

Theorem cygznlem3 16901
Description: A cyclic group with elements is isomorphic to . (Contributed by Mario Carneiro, 21-Apr-2016.)
Hypotheses
Ref Expression
cygzn.b
cygzn.n
cygzn.y
cygzn.m
cygzn.l
cygzn.e
cygzn.g
cygzn.x
cygzn.f
Assertion
Ref Expression
cygznlem3
Distinct variable groups:   , , ,   , , ,   , , ,   , , ,   , , ,   ,N   ,   , ,   , , ,
Allowed substitution hints:   ( , )   ( , , )   ( )   N( , )

Proof of Theorem cygznlem3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2443 . . . 4
2 cygzn.b . . . 4
3 eqid 2443 . . . 4
4 eqid 2443 . . . 4
5 cygzn.n . . . . . 6
6 hashcl 11690 . . . . . . . 8
76adantl 454 . . . . . . 7
8 0nn0 10287 . . . . . . . 8
98a1i 11 . . . . . . 7
107, 9ifclda 3792 . . . . . 6
115, 10syl5eqel 2527 . . . . 5
12 cygzn.y . . . . . 6
1312zncrng 16876 . . . . 5
14 crngrng 15725 . . . . 5
15 rnggrp 15720 . . . . 5
1611, 13, 14, 154syl 20 . . . 4
17 cygzn.g . . . . 5
18 cyggrp 15550 . . . . 5
1917, 18syl 16 . . . 4
20 cygzn.m . . . . 5
21 cygzn.l . . . . 5
22 cygzn.e . . . . 5
23 cygzn.x . . . . 5
24 cygzn.f . . . . 5
252, 5, 12, 20, 21, 22, 17, 23, 24cygznlem2a 16899 . . . 4
2612, 1, 21znzrhfo 16879 . . . . . . . 8
2711, 26syl 16 . . . . . . 7
28 foelrn 5936 . . . . . . 7
2927, 28sylan 459 . . . . . 6
30 foelrn 5936 . . . . . . 7
3127, 30sylan 459 . . . . . 6
3229, 31anim12dan 812 . . . . 5
33 reeanv 2882 . . . . . . 7
3419adantr 453 . . . . . . . . . . 11
35 simprl 734 . . . . . . . . . . 11
36 simprr 735 . . . . . . . . . . 11
372, 20, 22iscyggen 15541 . . . . . . . . . . . . . 14
3837simplbi 448 . . . . . . . . . . . . 13
3923, 38syl 16 . . . . . . . . . . . 12
4039adantr 453 . . . . . . . . . . 11
412, 20, 4mulgdir 14966 . . . . . . . . . . 11
4234, 35, 36, 40, 41syl13anc 1187 . . . . . . . . . 10
4311, 13syl 16 . . . . . . . . . . . . . . 15
44 eqid 2443 . . . . . . . . . . . . . . . 16
4544, 21zrhrhm 16844 . . . . . . . . . . . . . . 15
46 rhmghm 15877 . . . . . . . . . . . . . . 15
4743, 14, 45, 464syl 20 . . . . . . . . . . . . . 14
4847adantr 453 . . . . . . . . . . . . 13
49 zsubrg 16803 . . . . . . . . . . . . . . 15
5044subrgbas 15928 . . . . . . . . . . . . . . 15
5149, 50ax-mp 5 . . . . . . . . . . . . . 14
52 zex 10342 . . . . . . . . . . . . . . 15
53 cnfldadd 16759 . . . . . . . . . . . . . . . 16
5444, 53ressplusg 13622 . . . . . . . . . . . . . . 15
5552, 54ax-mp 5 . . . . . . . . . . . . . 14
5651, 55, 3ghmlin 15062 . . . . . . . . . . . . 13
5748, 35, 36, 56syl3anc 1185 . . . . . . . . . . . 12
5857fveq2d 5779 . . . . . . . . . . 11
59 zaddcl 10368 . . . . . . . . . . . 12
602, 5, 12, 20, 21, 22, 17, 23, 24cygznlem2 16900 . . . . . . . . . . . 12
6159, 60sylan2 462 . . . . . . . . . . 11
6258, 61eqtr3d 2477 . . . . . . . . . 10
632, 5, 12, 20, 21, 22, 17, 23, 24cygznlem2 16900 . . . . . . . . . . . 12
6463adantrr 699 . . . . . . . . . . 11
652, 5, 12, 20, 21, 22, 17, 23, 24cygznlem2 16900 . . . . . . . . . . . 12
6665adantrl 698 . . . . . . . . . . 11
6764, 66oveq12d 6147 . . . . . . . . . 10
6842, 62, 673eqtr4d 2485 . . . . . . . . 9
69 oveq12 6138 . . . . . . . . . . 11
7069fveq2d 5779 . . . . . . . . . 10
71 fveq2 5775 . . . . . . . . . . 11
72 fveq2 5775 . . . . . . . . . . 11
7371, 72oveqan12d 6148 . . . . . . . . . 10
7470, 73eqeq12d 2457 . . . . . . . . 9
7568, 74syl5ibrcom 215 . . . . . . . 8
7675rexlimdvva 2844 . . . . . . 7
7733, 76syl5bir 211 . . . . . 6
7877imp 420 . . . . 5
7932, 78syldan 458 . . . 4
801, 2, 3, 4, 16, 19, 25, 79isghmd 15066 . . 3
8164, 66eqeq12d 2457 . . . . . . . . . . . . 13
822, 5, 12, 20, 21, 22, 17, 23cygznlem1 16898 . . . . . . . . . . . . 13
8381, 82bitr4d 249 . . . . . . . . . . . 12
8483biimpd 200 . . . . . . . . . . 11
8571, 72eqeqan12d 2458 . . . . . . . . . . . 12
86 eqeq12 2455 . . . . . . . . . . . 12
8785, 86imbi12d 313 . . . . . . . . . . 11
8884, 87syl5ibrcom 215 . . . . . . . . . 10
8988rexlimdvva 2844 . . . . . . . . 9
9033, 89syl5bir 211 . . . . . . . 8
9190imp 420 . . . . . . 7
9232, 91syldan 458 . . . . . 6
9392ralrimivva 2805 . . . . 5
94 dff13 6052 . . . . 5
9525, 93, 94sylanbrc 647 . . . 4
962, 20, 22iscyggen2 15542 . . . . . . . . 9
9719, 96syl 16 . . . . . . . 8
9823, 97mpbid 203 . . . . . . 7
9998simprd 451 . . . . . 6
100 oveq1 6136 . . . . . . . . . 10
101100eqeq2d 2454 . . . . . . . . 9
102101cbvrexv 2942 . . . . . . . 8
10327adantr 453 . . . . . . . . . . . . 13
104 fof 5700 . . . . . . . . . . . . 13
105103, 104syl 16 . . . . . . . . . . . 12
106105ffvelrnda 5918 . . . . . . . . . . 11
10765adantlr 697 . . . . . . . . . . . 12
108107eqcomd 2448 . . . . . . . . . . 11
109 fveq2 5775 . . . . . . . . . . . . 13
110109eqeq2d 2454 . . . . . . . . . . . 12
111110rspcev 3061 . . . . . . . . . . 11
112106, 108, 111syl2anc 644 . . . . . . . . . 10
113 eqeq1 2449 . . . . . . . . . . 11
114113rexbidv 2733 . . . . . . . . . 10
115112, 114syl5ibrcom 215 . . . . . . . . 9
116115rexlimdva 2837 . . . . . . . 8
117102, 116syl5bi 210 . . . . . . 7
118117ralimdva 2791 . . . . . 6
11999, 118mpd 15 . . . . 5
120 dffo3 5932 . . . . 5
12125, 119, 120sylanbrc 647 . . . 4
122 df-f1o 5508 . . . 4
12395, 121, 122sylanbrc 647 . . 3
1241, 2isgim 15100 . . 3
12580, 123, 124sylanbrc 647 . 2
126 brgici 15108 . 2
127 gicsym 15112 . 2
128125, 126, 1273syl 19 1
Colors of variables: wff set class
Syntax hints:  -.wn 3  ->wi 4  <->wb 178  /\wa 360  =wceq 1654  e.wcel 1728  A.wral 2712  E.wrex 2713  {crab 2716   cvv 2965  ifcif 3765  <.cop 3844   class class class wbr 4243  e.cmpt 4301  rancrn 4920  -->wf 5497  -1-1->wf1 5498  -onto->wfo 5499  -1-1-onto->wf1o 5500  `cfv 5501  (class class class)co 6129   cfn 7158  0cc0 9041   caddc 9044   cn0 10272   cz 10333   chash 11669   cbs 13520   cress 13521   cplusg 13580   cgrp 14736   cmg 14740   cghm 15054   cgim 15095   cgic 15096   ccyg 15538   crg 15711   ccrg 15712   crh 15868   csubrg 15915   ccnfld 16754   czrh 16829   czn 16832
This theorem is referenced by:  cygzn  16902
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-rep 4354  ax-sep 4364  ax-nul 4372  ax-pow 4416  ax-pr 4442  ax-un 4742  ax-inf2 7645  ax-cnex 9097  ax-resscn 9098  ax-1cn 9099  ax-icn 9100  ax-addcl 9101  ax-addrcl 9102  ax-mulcl 9103  ax-mulrcl 9104  ax-mulcom 9105  ax-addass 9106  ax-mulass 9107  ax-distr 9108  ax-i2m1 9109  ax-1ne0 9110  ax-1rid 9111  ax-rnegex 9112  ax-rrecex 9113  ax-cnre 9114  ax-pre-lttri 9115  ax-pre-lttrn 9116  ax-pre-ltadd 9117  ax-pre-mulgt0 9118  ax-pre-sup 9119  ax-addf 9120  ax-mulf 9121
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2717  df-rex 2718  df-reu 2719  df-rmo 2720  df-rab 2721  df-v 2967  df-sbc 3171  df-csb 3271  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-pss 3325  df-nul 3617  df-if 3766  df-pw 3828  df-sn 3847  df-pr 3848  df-tp 3849  df-op 3850  df-uni 4044  df-int 4080  df-iun 4124  df-br 4244  df-opab 4302  df-mpt 4303  df-tr 4337  df-eprel 4535  df-id 4539  df-po 4544  df-so 4545  df-fr 4582  df-se 4583  df-we 4584  df-ord 4625  df-on 4626  df-lim 4627  df-suc 4628  df-om 4887  df-xp 4925  df-rel 4926  df-cnv 4927  df-co 4928  df-dm 4929  df-rn 4930  df-res 4931  df-ima 4932  df-iota 5464  df-fun 5503  df-fn 5504  df-f 5505  df-f1 5506  df-fo 5507  df-f1o 5508  df-fv 5509  df-isom 5510  df-ov 6132  df-oprab 6133  df-mpt2 6134  df-1st 6399  df-2nd 6400  df-tpos 6529  df-riota 6599  df-recs 6682  df-rdg 6717  df-1o 6773  df-oadd 6777  df-omul 6778  df-er 6954  df-ec 6956  df-qs 6960  df-map 7069  df-en 7159  df-dom 7160  df-sdom 7161  df-fin 7162  df-sup 7495  df-oi 7528  df-card 7877  df-acn 7880  df-pnf 9173  df-mnf 9174  df-xr 9175  df-ltxr 9176  df-le 9177  df-sub 9344  df-neg 9345  df-div 9729  df-nn 10052  df-2 10109  df-3 10110  df-4 10111  df-5 10112  df-6 10113  df-7 10114  df-8 10115  df-9 10116  df-10 10117  df-n0 10273  df-z 10334  df-dec 10434  df-uz 10540  df-rp 10664  df-fz 11095  df-fl 11253  df-mod 11302  df-seq 11375  df-exp 11434  df-hash 11670  df-cj 11955  df-re 11956  df-im 11957  df-sqr 12091  df-abs 12092  df-dvds 12904  df-struct 13522  df-ndx 13523  df-slot 13524  df-base 13525  df-sets 13526  df-ress 13527  df-plusg 13593  df-mulr 13594  df-starv 13595  df-sca 13596  df-vsca 13597  df-tset 13599  df-ple 13600  df-ds 13602  df-unif 13603  df-0g 13778  df-imas 13785  df-divs 13786  df-mnd 14741  df-mhm 14789  df-grp 14863  df-minusg 14864  df-sbg 14865  df-mulg 14866  df-subg 14992  df-nsg 14993  df-eqg 14994  df-ghm 15055  df-gim 15097  df-gic 15098  df-od 15218  df-cmn 15465  df-abl 15466  df-cyg 15539  df-mgp 15700  df-rng 15714  df-cring 15715  df-ur 15716  df-oppr 15779  df-dvdsr 15797  df-rnghom 15870  df-subrg 15917  df-lmod 16003  df-lss 16060  df-lsp 16099  df-sra 16295  df-rgmod 16296  df-lidl 16297  df-rsp 16298  df-2idl 16354  df-cnfld 16755  df-zrh 16833  df-zn 16836
  Copyright terms: Public domain W3C validator