Theorem zncrng 21519

Description: ℤ/nℤ is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.)

Hypothesis

Ref	Expression
zncrng.y	⊢ 𝑌 = (ℤ/nℤ‘𝑁)

Assertion

Ref	Expression
zncrng	⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CRing)

Proof of Theorem zncrng

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nn0z 12539	. . 3 ⊢ (𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ)
2		eqid 2739	. . . 4 ⊢ (RSpan‘ℤring) = (RSpan‘ℤring)
3		eqid 2739	. . . 4 ⊢ (ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁}))) = (ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁})))
4	2, 3	zncrng2 21509	. . 3 ⊢ (𝑁 ∈ ℤ → (ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁}))) ∈ CRing)
5	1, 4	syl 17	. 2 ⊢ (𝑁 ∈ ℕ0 → (ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁}))) ∈ CRing)
6		eqidd 2740	. . 3 ⊢ (𝑁 ∈ ℕ0 → (Base‘(ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁})))) = (Base‘(ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁})))))
7		zncrng.y	. . . 4 ⊢ 𝑌 = (ℤ/nℤ‘𝑁)
8	2, 3, 7	znbas2 21514	. . 3 ⊢ (𝑁 ∈ ℕ0 → (Base‘(ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁})))) = (Base‘𝑌))
9	2, 3, 7	znadd 21515	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (+g‘(ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁})))) = (+g‘𝑌))
10	9	oveqdr 7384	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ (Base‘(ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁})))) ∧ 𝑦 ∈ (Base‘(ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁})))))) → (𝑥(+g‘(ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁}))))𝑦) = (𝑥(+g‘𝑌)𝑦))
11	2, 3, 7	znmul 21516	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (.r‘(ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁})))) = (.r‘𝑌))
12	11	oveqdr 7384	. . 3 ⊢ ((𝑁 ∈ ℕ0 ∧ (𝑥 ∈ (Base‘(ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁})))) ∧ 𝑦 ∈ (Base‘(ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁})))))) → (𝑥(.r‘(ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁}))))𝑦) = (𝑥(.r‘𝑌)𝑦))
13	6, 8, 10, 12	crngpropd 20261	. 2 ⊢ (𝑁 ∈ ℕ0 → ((ℤring /s (ℤring ~QG ((RSpan‘ℤring)‘{𝑁}))) ∈ CRing ↔ 𝑌 ∈ CRing))
14	5, 13	mpbid 233	1 ⊢ (𝑁 ∈ ℕ0 → 𝑌 ∈ CRing)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {csn 4555  ‘cfv 6485  (class class class)co 7356  ℕ₀cn0 12428  ℤcz 12515  Basecbs 17170  +_gcplusg 17211  ._rcmulr 17212   /_s cqus 17460   ~_QG cqg 19089  CRingccrg 20206  RSpancrsp 21200  ℤ_ringczring 21421  ℤ/nℤczn 21477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106  ax-addf 11108

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-tpos 8166  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-er 8633  df-ec 8635  df-qs 8639  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9345  df-inf 9346  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-z 12516  df-dec 12636  df-uz 12780  df-fz 13453  df-struct 17108  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192  df-plusg 17224  df-mulr 17225  df-starv 17226  df-sca 17227  df-vsca 17228  df-ip 17229  df-tset 17230  df-ple 17231  df-ds 17233  df-unif 17234  df-0g 17395  df-imas 17463  df-qus 17464  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-grp 18903  df-minusg 18904  df-sbg 18905  df-subg 19090  df-nsg 19091  df-eqg 19092  df-cmn 19748  df-abl 19749  df-mgp 20113  df-rng 20125  df-ur 20154  df-ring 20207  df-cring 20208  df-oppr 20308  df-subrng 20518  df-subrg 20542  df-lmod 20852  df-lss 20922  df-lsp 20962  df-sra 21163  df-rgmod 21164  df-lidl 21201  df-rsp 21202  df-2idl 21243  df-cnfld 21348  df-zring 21422  df-zn 21481

This theorem is referenced by:  zncyg  21523  zndvds0  21525  znf1o  21526  zzngim  21527  znfld  21535  znchr  21537  znunit  21538  znrrg  21540  cygznlem3  21544  dchrelbas3  27219  dchrelbasd  27220  dchrzrh1  27225  dchrzrhmul  27227  dchrmulcl  27230  dchrn0  27231  dchrfi  27236  dchrghm  27237  dchrabs  27241  dchrinv  27242  dchrptlem1  27245  dchrptlem2  27246  dchrptlem3  27247  dchrpt  27248  dchrsum2  27249  dchrhash  27252  sum2dchr  27255  lgsdchr  27336  dchrisum0flblem1  27489  dchrisum0re  27494  znfermltl  33449  ply1fermltl  33669  hashscontpowcl  42605  hashscontpow  42607  aks6d1c4  42609  aks6d1c2  42615  aks6d1c6lem3  42657  aks6d1c6lem5  42662  aks6d1c7lem1  42665  aks5lem2  42672  aks5lem3a  42674  aks5lem5a  42676  frlmpwfi  43543  isnumbasgrplem3  43550  cznabel  48751  cznrng  48752