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

Theorem frgpcyg 16529
 Description: A free group is cyclic iff it has zero or one generator. (Contributed by Mario Carneiro, 21-Apr-2016.)
Hypothesis
Ref Expression
frgpcyg.g freeGrp
Assertion
Ref Expression
frgpcyg CycGrp

Proof of Theorem frgpcyg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 brdom2 6893 . . 3
2 sdom1 7064 . . . . 5
3 frgpcyg.g . . . . . . 7 freeGrp
4 fveq2 5527 . . . . . . 7 freeGrp freeGrp
53, 4syl5eq 2329 . . . . . 6 freeGrp
6 0ex 4152 . . . . . . . 8
7 eqid 2285 . . . . . . . . 9 freeGrp freeGrp
87frgpgrp 15073 . . . . . . . 8 freeGrp
96, 8ax-mp 8 . . . . . . 7 freeGrp
10 eqid 2285 . . . . . . . 8 freeGrp freeGrp
117, 100frgp 15090 . . . . . . 7 freeGrp
12100cyg 15181 . . . . . . 7 freeGrp freeGrp freeGrp CycGrp
139, 11, 12mp2an 653 . . . . . 6 freeGrp CycGrp
145, 13syl6eqel 2373 . . . . 5 CycGrp
152, 14sylbi 187 . . . 4 CycGrp
16 eqid 2285 . . . . 5
17 eqid 2285 . . . . 5 .g .g
18 relen 6870 . . . . . . 7
1918brrelexi 4731 . . . . . 6
203frgpgrp 15073 . . . . . 6
2119, 20syl 15 . . . . 5
22 eqid 2285 . . . . . . . 8 ~FG ~FG
23 eqid 2285 . . . . . . . 8 varFGrp varFGrp
2422, 23, 3, 16vrgpf 15079 . . . . . . 7 varFGrp
2519, 24syl 15 . . . . . 6 varFGrp
26 en1b 6931 . . . . . . . 8
27 eqimss2 3233 . . . . . . . 8
2826, 27sylbi 187 . . . . . . 7
29 uniexg 4519 . . . . . . . . 9
3019, 29syl 15 . . . . . . . 8
31 snssg 3756 . . . . . . . 8
3230, 31syl 15 . . . . . . 7
3328, 32mpbird 223 . . . . . 6
34 ffvelrn 5665 . . . . . 6 varFGrp varFGrp
3525, 33, 34syl2anc 642 . . . . 5 varFGrp
36 zsubrg 16427 . . . . . . . . . . 11 SubRingfld
37 subrgsubg 15553 . . . . . . . . . . 11 SubRingfld SubGrpfld
3836, 37ax-mp 8 . . . . . . . . . 10 SubGrpfld
39 eqid 2285 . . . . . . . . . . 11 flds flds
4039subggrp 14626 . . . . . . . . . 10 SubGrpfld flds
4138, 40mp1i 11 . . . . . . . . 9 flds
42 1z 10055 . . . . . . . . . . . . 13
43 f1osng 5516 . . . . . . . . . . . . 13
4430, 42, 43sylancl 643 . . . . . . . . . . . 12
45 f1of 5474 . . . . . . . . . . . 12
4644, 45syl 15 . . . . . . . . . . 11
4726biimpi 186 . . . . . . . . . . . 12
4847feq2d 5382 . . . . . . . . . . 11
4946, 48mpbird 223 . . . . . . . . . 10
50 snssi 3761 . . . . . . . . . . 11
5142, 50ax-mp 8 . . . . . . . . . 10
52 fss 5399 . . . . . . . . . 10
5349, 51, 52sylancl 643 . . . . . . . . 9
5439subrgbas 15556 . . . . . . . . . . 11 SubRingfld flds
5536, 54ax-mp 8 . . . . . . . . . 10 flds
563, 55, 23frgpup3 15089 . . . . . . . . 9 flds flds varFGrp
5741, 19, 53, 56syl3anc 1182 . . . . . . . 8 flds varFGrp
5857adantr 451 . . . . . . 7 flds varFGrp
59 reurex 2756 . . . . . . 7 flds varFGrp flds varFGrp
6058, 59syl 15 . . . . . 6 flds varFGrp
61 fveq1 5526 . . . . . . . . . 10 varFGrp varFGrp
62 fvco3 5598 . . . . . . . . . . . 12 varFGrp varFGrp varFGrp
6325, 33, 62syl2anc 642 . . . . . . . . . . 11 varFGrp varFGrp
64 fvsng 5716 . . . . . . . . . . . 12
6530, 42, 64sylancl 643 . . . . . . . . . . 11
6663, 65eqeq12d 2299 . . . . . . . . . 10 varFGrp varFGrp
6761, 66syl5ib 210 . . . . . . . . 9 varFGrp varFGrp
6867ad2antrr 706 . . . . . . . 8 flds varFGrp varFGrp
6916, 55ghmf 14689 . . . . . . . . . . . . 13 flds
7069ad2antrl 708 . . . . . . . . . . . 12 flds varFGrp
71 ffvelrn 5665 . . . . . . . . . . . 12
7270, 71sylan 457 . . . . . . . . . . 11 flds varFGrp
7372an32s 779 . . . . . . . . . 10 flds varFGrp
74 mptresid 5006 . . . . . . . . . . . . . 14
753, 16, 23frgpup3 15089 . . . . . . . . . . . . . . . . . 18 varFGrp varFGrp varFGrp
7621, 19, 25, 75syl3anc 1182 . . . . . . . . . . . . . . . . 17 varFGrp varFGrp
77 reu5 2755 . . . . . . . . . . . . . . . . . 18 varFGrp varFGrp varFGrp varFGrp varFGrp varFGrp
7877simprbi 450 . . . . . . . . . . . . . . . . 17 varFGrp varFGrp varFGrp varFGrp
7976, 78syl 15 . . . . . . . . . . . . . . . 16 varFGrp varFGrp
8079adantr 451 . . . . . . . . . . . . . . 15 flds varFGrp varFGrp varFGrp
8121adantr 451 . . . . . . . . . . . . . . . 16 flds varFGrp
8216idghm 14700 . . . . . . . . . . . . . . . 16
8381, 82syl 15 . . . . . . . . . . . . . . 15 flds varFGrp
8425adantr 451 . . . . . . . . . . . . . . . 16 flds varFGrp varFGrp
85 fcoi2 5418 . . . . . . . . . . . . . . . 16 varFGrp varFGrp varFGrp
8684, 85syl 15 . . . . . . . . . . . . . . 15 flds varFGrp varFGrp varFGrp
8770feqmptd 5577 . . . . . . . . . . . . . . . . 17 flds varFGrp
88 eqidd 2286 . . . . . . . . . . . . . . . . 17 flds varFGrp .gvarFGrp .gvarFGrp
89 oveq1 5867 . . . . . . . . . . . . . . . . 17 .gvarFGrp .gvarFGrp
9072, 87, 88, 89fmptco 5693 . . . . . . . . . . . . . . . 16 flds varFGrp .gvarFGrp .gvarFGrp
9135adantr 451 . . . . . . . . . . . . . . . . . 18 flds varFGrp varFGrp
92 eqid 2285 . . . . . . . . . . . . . . . . . . 19 .gvarFGrp .gvarFGrp
9339, 17, 92, 16mulgghm2 16461 . . . . . . . . . . . . . . . . . 18 varFGrp .gvarFGrp flds
9481, 91, 93syl2anc 642 . . . . . . . . . . . . . . . . 17 flds varFGrp .gvarFGrp flds
95 simprl 732 . . . . . . . . . . . . . . . . 17 flds varFGrp flds
96 ghmco 14704 . . . . . . . . . . . . . . . . 17 .gvarFGrp flds flds .gvarFGrp
9794, 95, 96syl2anc 642 . . . . . . . . . . . . . . . 16 flds varFGrp .gvarFGrp
9890, 97eqeltrrd 2360 . . . . . . . . . . . . . . 15 flds varFGrp .gvarFGrp
9947adantr 451 . . . . . . . . . . . . . . . . . . . 20 flds varFGrp
10099eleq2d 2352 . . . . . . . . . . . . . . . . . . 19 flds varFGrp
101 simprr 733 . . . . . . . . . . . . . . . . . . . . . 22 flds varFGrp varFGrp
102101oveq1d 5875 . . . . . . . . . . . . . . . . . . . . 21 flds varFGrp varFGrp.gvarFGrp .gvarFGrp
10316, 17mulg1 14576 . . . . . . . . . . . . . . . . . . . . . 22 varFGrp .gvarFGrp varFGrp
10491, 103syl 15 . . . . . . . . . . . . . . . . . . . . 21 flds varFGrp .gvarFGrp varFGrp
105102, 104eqtrd 2317 . . . . . . . . . . . . . . . . . . . 20 flds varFGrp varFGrp.gvarFGrp varFGrp
106 elsni 3666 . . . . . . . . . . . . . . . . . . . . . . . 24
107106fveq2d 5531 . . . . . . . . . . . . . . . . . . . . . . 23 varFGrp varFGrp
108107fveq2d 5531 . . . . . . . . . . . . . . . . . . . . . 22 varFGrp varFGrp
109108oveq1d 5875 . . . . . . . . . . . . . . . . . . . . 21 varFGrp.gvarFGrp varFGrp.gvarFGrp
110109, 107eqeq12d 2299 . . . . . . . . . . . . . . . . . . . 20 varFGrp.gvarFGrp varFGrp varFGrp.gvarFGrp varFGrp
111105, 110syl5ibrcom 213 . . . . . . . . . . . . . . . . . . 19 flds varFGrp varFGrp.gvarFGrp varFGrp
112100, 111sylbid 206 . . . . . . . . . . . . . . . . . 18 flds varFGrp varFGrp.gvarFGrp varFGrp
113112imp 418 . . . . . . . . . . . . . . . . 17 flds varFGrp varFGrp.gvarFGrp varFGrp
114113mpteq2dva 4108 . . . . . . . . . . . . . . . 16 flds varFGrp varFGrp.gvarFGrp varFGrp
115 ffvelrn 5665 . . . . . . . . . . . . . . . . . 18 varFGrp varFGrp
11684, 115sylan 457 . . . . . . . . . . . . . . . . 17 flds varFGrp varFGrp
11784feqmptd 5577 . . . . . . . . . . . . . . . . 17 flds varFGrp varFGrp varFGrp
118 eqidd 2286 . . . . . . . . . . . . . . . . 17 flds varFGrp .gvarFGrp .gvarFGrp
119 fveq2 5527 . . . . . . . . . . . . . . . . . 18 varFGrp varFGrp
120119oveq1d 5875 . . . . . . . . . . . . . . . . 17 varFGrp .gvarFGrp varFGrp.gvarFGrp
121116, 117, 118, 120fmptco 5693 . . . . . . . . . . . . . . . 16 flds varFGrp .gvarFGrp varFGrp varFGrp.gvarFGrp
122114, 121, 1173eqtr4d 2327 . . . . . . . . . . . . . . 15 flds varFGrp .gvarFGrp varFGrp varFGrp
123 coeq1 4843 . . . . . . . . . . . . . . . . 17 varFGrp varFGrp
124123eqeq1d 2293 . . . . . . . . . . . . . . . 16 varFGrp varFGrp varFGrp varFGrp
125 coeq1 4843 . . . . . . . . . . . . . . . . 17 .gvarFGrp varFGrp .gvarFGrp varFGrp
126125eqeq1d 2293 . . . . . . . . . . . . . . . 16 .gvarFGrp varFGrp varFGrp .gvarFGrp varFGrp varFGrp
127124, 126rmoi 3082 . . . . . . . . . . . . . . 15 varFGrp varFGrp varFGrp varFGrp .gvarFGrp .gvarFGrp varFGrp varFGrp .gvarFGrp
12880, 83, 86, 98, 122, 127syl122anc 1191 . . . . . . . . . . . . . 14 flds varFGrp .gvarFGrp
12974, 128syl5eq 2329 . . . . . . . . . . . . 13 flds varFGrp .gvarFGrp
130 mpteqb 5616 . . . . . . . . . . . . . 14 .gvarFGrp .gvarFGrp
131 id 19 . . . . . . . . . . . . . 14
132130, 131mprg 2614 . . . . . . . . . . . . 13 .gvarFGrp .gvarFGrp
133129, 132sylib 188 . . . . . . . . . . . 12 flds varFGrp .gvarFGrp
134133r19.21bi 2643 . . . . . . . . . . 11 flds varFGrp .gvarFGrp
135134an32s 779 . . . . . . . . . 10 flds varFGrp .gvarFGrp
13689eqeq2d 2296 . . . . . . . . . . 11 .gvarFGrp .gvarFGrp
137136rspcev 2886 . . . . . . . . . 10 .gvarFGrp .gvarFGrp
13873, 135, 137syl2anc 642 . . . . . . . . 9 flds varFGrp .gvarFGrp
139138expr 598 . . . . . . . 8 flds varFGrp .gvarFGrp
14068, 139syld 40 . . . . . . 7 flds varFGrp .gvarFGrp
141140rexlimdva 2669 . . . . . 6 flds varFGrp .gvarFGrp
14260, 141mpd 14 . . . . 5 .gvarFGrp
14316, 17, 21, 35, 142iscygd 15176 . . . 4 CycGrp
14415, 143jaoi 368 . . 3 CycGrp
1451, 144sylbi 187 . 2 CycGrp
146 cygabl 15179 . . 3 CycGrp
1473frgpnabl 15165 . . . . 5
148147con2i 112 . . . 4
149 ablgrp 15096 . . . . . 6
150 eqid 2285 . . . . . . 7
15116, 150grpidcl 14512 . . . . . 6
1523, 16elbasfv 13193 . . . . . 6
153149, 151, 1523syl 18 . . . . 5
154 1onn 6639 . . . . . 6
155 nnfi 7055 . . . . . 6
156154, 155ax-mp 8 . . . . 5
157 fidomtri2 7629 . . . . 5
158153, 156, 157sylancl 643 . . . 4
159148, 158mpbird 223 . . 3
160146, 159syl 15 . 2 CycGrp
161145, 160impbii 180 1 CycGrp
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358   wceq 1625   wcel 1686  wral 2545  wrex 2546  wreu 2547  wrmo 2548  cvv 2790   wss 3154  c0 3457  csn 3642  cop 3645  cuni 3829   class class class wbr 4025   cmpt 4079   cid 4306  com 4658   cres 4693   ccom 4695  wf 5253  wf1o 5256  cfv 5257  (class class class)co 5860  c1o 6474   cen 6862   cdom 6863   csdm 6864  cfn 6865  c1 8740  cz 10026  cbs 13150   ↾s cress 13151  c0g 13402  cgrp 14364  .gcmg 14368  SubGrpcsubg 14617   cghm 14682   ~FG cefg 15017  freeGrpcfrgp 15018  varFGrpcvrgp 15019  cabel 15092  CycGrpccyg 15166  SubRingcsubrg 15543  ℂfldccnfld 16379 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-inf2 7344  ax-cnex 8795  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-mulcom 8803  ax-addass 8804  ax-mulass 8805  ax-distr 8806  ax-i2m1 8807  ax-1ne0 8808  ax-1rid 8809  ax-rnegex 8810  ax-rrecex 8811  ax-cnre 8812  ax-pre-lttri 8813  ax-pre-lttrn 8814  ax-pre-ltadd 8815  ax-pre-mulgt0 8816  ax-addf 8818  ax-mulf 8819 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 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rmo 2553  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-ot 3652  df-uni 3830  df-int 3865  df-iun 3909  df-iin 3910  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-1st 6124  df-2nd 6125  df-riota 6306  df-recs 6390  df-rdg 6425  df-1o 6481  df-2o 6482  df-oadd 6485  df-er 6662  df-ec 6664  df-qs 6668  df-map 6776  df-pm 6777  df-en 6866  df-dom 6867  df-sdom 6868  df-fin 6869  df-sup 7196  df-card 7574  df-pnf 8871  df-mnf 8872  df-xr 8873  df-ltxr 8874  df-le 8875  df-sub 9041  df-neg 9042  df-nn 9749  df-2 9806  df-3 9807  df-4 9808  df-5 9809  df-6 9810  df-7 9811  df-8 9812  df-9 9813  df-10 9814  df-n0 9968  df-z 10027  df-dec 10127  df-uz 10233  df-rp 10357  df-fz 10785  df-fzo 10873  df-seq 11049  df-hash 11340  df-word 11411  df-concat 11412  df-s1 11413  df-substr 11414  df-splice 11415  df-reverse 11416  df-s2 11500  df-struct 13152  df-ndx 13153  df-slot 13154  df-base 13155  df-sets 13156  df-ress 13157  df-plusg 13223  df-mulr 13224  df-starv 13225  df-sca 13226  df-vsca 13227  df-tset 13229  df-ple 13230  df-ds 13232  df-0g 13406  df-gsum 13407  df-imas 13413  df-divs 13414  df-mnd 14369  df-mhm 14417  df-submnd 14418  df-frmd 14473  df-vrmd 14474  df-grp 14491  df-minusg 14492  df-mulg 14494  df-subg 14620  df-ghm 14683  df-efg 15020  df-frgp 15021  df-vrgp 15022  df-cmn 15093  df-abl 15094  df-cyg 15167  df-mgp 15328  df-rng 15342  df-cring 15343  df-ur 15344  df-subrg 15545  df-cnfld 16380
 Copyright terms: Public domain W3C validator