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

Theorem zzngim 16774
 Description: The ring homomorphism is an isomorphism for . (We only show group isomorphism here, but ring isomorphism follows, since it is a bijective ring homomorphism.) (Contributed by Mario Carneiro, 21-Apr-2016.)
Hypotheses
Ref Expression
zzngim.y ℤ/n
zzngim.2 RHom
Assertion
Ref Expression
zzngim flds GrpIso

Proof of Theorem zzngim
StepHypRef Expression
1 0nn0 10182 . . . 4
2 zzngim.y . . . . 5 ℤ/n
32zncrng 16766 . . . 4
4 crngrng 15615 . . . 4
51, 3, 4mp2b 10 . . 3
6 eqid 2401 . . . 4 flds flds
7 zzngim.2 . . . 4 RHom
86, 7zrhrhm 16734 . . 3 flds RingHom
9 rhmghm 15767 . . 3 flds RingHom flds
105, 8, 9mp2b 10 . 2 flds
11 eqid 2401 . . . 4
122, 11, 7znzrhfo 16769 . . . . . . 7
131, 12ax-mp 8 . . . . . 6
14 fofn 5609 . . . . . 6
15 fnresdm 5508 . . . . . 6
1613, 14, 15mp2b 10 . . . . 5
177reseq1i 5096 . . . . 5 RHom
1816, 17eqtr3i 2423 . . . 4 RHom
19 eqid 2401 . . . . . 6
20 iftrue 3702 . . . . . 6 ..^
2119, 20ax-mp 8 . . . . 5 ..^
2221eqcomi 2405 . . . 4 ..^
236, 2, 11, 18, 22znf1o 16773 . . 3
241, 23ax-mp 8 . 2
25 zsubrg 16693 . . . 4 SubRingfld
266subrgbas 15818 . . . 4 SubRingfld flds
2725, 26ax-mp 8 . . 3 flds
2827, 11isgim 14990 . 2 flds GrpIso flds
2910, 24, 28mpbir2an 887 1 flds GrpIso
 Colors of variables: wff set class Syntax hints:   wceq 1649   wcel 1721  cif 3696   cres 4834   wfn 5403  wfo 5406  wf1o 5407  cfv 5408  (class class class)co 6034  cc0 8937  cn0 10167  cz 10228  ..^cfzo 11079  cbs 13410   ↾s cress 13411   cghm 14944   GrpIso cgim 14985  crg 15601  ccrg 15602   RingHom crh 15758  SubRingcsubrg 15805  ℂfldccnfld 16644  RHomczrh 16719  ℤ/nℤczn 16722 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2382  ax-rep 4275  ax-sep 4285  ax-nul 4293  ax-pow 4332  ax-pr 4358  ax-un 4655  ax-inf2 7543  ax-cnex 8993  ax-resscn 8994  ax-1cn 8995  ax-icn 8996  ax-addcl 8997  ax-addrcl 8998  ax-mulcl 8999  ax-mulrcl 9000  ax-mulcom 9001  ax-addass 9002  ax-mulass 9003  ax-distr 9004  ax-i2m1 9005  ax-1ne0 9006  ax-1rid 9007  ax-rnegex 9008  ax-rrecex 9009  ax-cnre 9010  ax-pre-lttri 9011  ax-pre-lttrn 9012  ax-pre-ltadd 9013  ax-pre-mulgt0 9014  ax-pre-sup 9015  ax-addf 9016  ax-mulf 9017 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2526  df-ne 2566  df-nel 2567  df-ral 2668  df-rex 2669  df-reu 2670  df-rmo 2671  df-rab 2672  df-v 2915  df-sbc 3119  df-csb 3209  df-dif 3280  df-un 3282  df-in 3284  df-ss 3291  df-pss 3293  df-nul 3586  df-if 3697  df-pw 3758  df-sn 3777  df-pr 3778  df-tp 3779  df-op 3780  df-uni 3972  df-int 4007  df-iun 4051  df-br 4168  df-opab 4222  df-mpt 4223  df-tr 4258  df-eprel 4449  df-id 4453  df-po 4458  df-so 4459  df-fr 4496  df-we 4498  df-ord 4539  df-on 4540  df-lim 4541  df-suc 4542  df-om 4800  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5372  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6037  df-oprab 6038  df-mpt2 6039  df-1st 6302  df-2nd 6303  df-tpos 6429  df-riota 6499  df-recs 6583  df-rdg 6618  df-1o 6674  df-oadd 6678  df-er 6855  df-ec 6857  df-qs 6861  df-map 6970  df-en 7060  df-dom 7061  df-sdom 7062  df-fin 7063  df-sup 7395  df-pnf 9069  df-mnf 9070  df-xr 9071  df-ltxr 9072  df-le 9073  df-sub 9239  df-neg 9240  df-div 9624  df-nn 9947  df-2 10004  df-3 10005  df-4 10006  df-5 10007  df-6 10008  df-7 10009  df-8 10010  df-9 10011  df-10 10012  df-n0 10168  df-z 10229  df-dec 10329  df-uz 10435  df-rp 10559  df-fz 10990  df-fzo 11080  df-fl 11143  df-mod 11192  df-seq 11265  df-dvds 12794  df-struct 13412  df-ndx 13413  df-slot 13414  df-base 13415  df-sets 13416  df-ress 13417  df-plusg 13483  df-mulr 13484  df-starv 13485  df-sca 13486  df-vsca 13487  df-tset 13489  df-ple 13490  df-ds 13492  df-unif 13493  df-0g 13668  df-imas 13675  df-divs 13676  df-mnd 14631  df-mhm 14679  df-grp 14753  df-minusg 14754  df-sbg 14755  df-mulg 14756  df-subg 14882  df-nsg 14883  df-eqg 14884  df-ghm 14945  df-gim 14987  df-cmn 15355  df-abl 15356  df-mgp 15590  df-rng 15604  df-cring 15605  df-ur 15606  df-oppr 15669  df-dvdsr 15687  df-rnghom 15760  df-subrg 15807  df-lmod 15893  df-lss 15950  df-lsp 15989  df-sra 16185  df-rgmod 16186  df-lidl 16187  df-rsp 16188  df-2idl 16244  df-cnfld 16645  df-zrh 16723  df-zn 16726
 Copyright terms: Public domain W3C validator