![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > irinitoringc | Structured version Visualization version GIF version |
Description: The ring of integers is an initial object in the category of unital rings (within a universe containing the ring of integers). Example 7.2 (6) of [Adamek] p. 101 , and example in [Lang] p. 58. (Contributed by AV, 3-Apr-2020.) |
Ref | Expression |
---|---|
irinitoringc.u | ⊢ (𝜑 → 𝑈 ∈ 𝑉) |
irinitoringc.z | ⊢ (𝜑 → ℤring ∈ 𝑈) |
irinitoringc.c | ⊢ 𝐶 = (RingCat‘𝑈) |
Ref | Expression |
---|---|
irinitoringc | ⊢ (𝜑 → ℤring ∈ (InitO‘𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zex 11840 | . . . . . 6 ⊢ ℤ ∈ V | |
2 | 1 | mptex 6855 | . . . . 5 ⊢ (𝑧 ∈ ℤ ↦ (𝑧(.g‘𝑟)(1r‘𝑟))) ∈ V |
3 | irinitoringc.c | . . . . . . . . 9 ⊢ 𝐶 = (RingCat‘𝑈) | |
4 | eqid 2794 | . . . . . . . . 9 ⊢ (Base‘𝐶) = (Base‘𝐶) | |
5 | irinitoringc.u | . . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ 𝑉) | |
6 | eqid 2794 | . . . . . . . . 9 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶) | |
7 | 3, 4, 5, 6 | ringchomfval 43775 | . . . . . . . 8 ⊢ (𝜑 → (Hom ‘𝐶) = ( RingHom ↾ ((Base‘𝐶) × (Base‘𝐶)))) |
8 | 7 | adantr 481 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (Hom ‘𝐶) = ( RingHom ↾ ((Base‘𝐶) × (Base‘𝐶)))) |
9 | 8 | oveqd 7036 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℤring(Hom ‘𝐶)𝑟) = (ℤring( RingHom ↾ ((Base‘𝐶) × (Base‘𝐶)))𝑟)) |
10 | irinitoringc.z | . . . . . . . . . 10 ⊢ (𝜑 → ℤring ∈ 𝑈) | |
11 | id 22 | . . . . . . . . . . 11 ⊢ (ℤring ∈ 𝑈 → ℤring ∈ 𝑈) | |
12 | zringring 20302 | . . . . . . . . . . . 12 ⊢ ℤring ∈ Ring | |
13 | 12 | a1i 11 | . . . . . . . . . . 11 ⊢ (ℤring ∈ 𝑈 → ℤring ∈ Ring) |
14 | 11, 13 | elind 4094 | . . . . . . . . . 10 ⊢ (ℤring ∈ 𝑈 → ℤring ∈ (𝑈 ∩ Ring)) |
15 | 10, 14 | syl 17 | . . . . . . . . 9 ⊢ (𝜑 → ℤring ∈ (𝑈 ∩ Ring)) |
16 | 3, 4, 5 | ringcbas 43774 | . . . . . . . . 9 ⊢ (𝜑 → (Base‘𝐶) = (𝑈 ∩ Ring)) |
17 | 15, 16 | eleqtrrd 2885 | . . . . . . . 8 ⊢ (𝜑 → ℤring ∈ (Base‘𝐶)) |
18 | 17 | adantr 481 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → ℤring ∈ (Base‘𝐶)) |
19 | simpr 485 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑟 ∈ (Base‘𝐶)) | |
20 | 18, 19 | ovresd 7174 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℤring( RingHom ↾ ((Base‘𝐶) × (Base‘𝐶)))𝑟) = (ℤring RingHom 𝑟)) |
21 | 16 | eleq2d 2867 | . . . . . . . . 9 ⊢ (𝜑 → (𝑟 ∈ (Base‘𝐶) ↔ 𝑟 ∈ (𝑈 ∩ Ring))) |
22 | elin 4092 | . . . . . . . . . 10 ⊢ (𝑟 ∈ (𝑈 ∩ Ring) ↔ (𝑟 ∈ 𝑈 ∧ 𝑟 ∈ Ring)) | |
23 | 22 | simprbi 497 | . . . . . . . . 9 ⊢ (𝑟 ∈ (𝑈 ∩ Ring) → 𝑟 ∈ Ring) |
24 | 21, 23 | syl6bi 254 | . . . . . . . 8 ⊢ (𝜑 → (𝑟 ∈ (Base‘𝐶) → 𝑟 ∈ Ring)) |
25 | 24 | imp 407 | . . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → 𝑟 ∈ Ring) |
26 | eqid 2794 | . . . . . . . 8 ⊢ (.g‘𝑟) = (.g‘𝑟) | |
27 | eqid 2794 | . . . . . . . 8 ⊢ (𝑧 ∈ ℤ ↦ (𝑧(.g‘𝑟)(1r‘𝑟))) = (𝑧 ∈ ℤ ↦ (𝑧(.g‘𝑟)(1r‘𝑟))) | |
28 | eqid 2794 | . . . . . . . 8 ⊢ (1r‘𝑟) = (1r‘𝑟) | |
29 | 26, 27, 28 | mulgrhm2 20328 | . . . . . . 7 ⊢ (𝑟 ∈ Ring → (ℤring RingHom 𝑟) = {(𝑧 ∈ ℤ ↦ (𝑧(.g‘𝑟)(1r‘𝑟)))}) |
30 | 25, 29 | syl 17 | . . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℤring RingHom 𝑟) = {(𝑧 ∈ ℤ ↦ (𝑧(.g‘𝑟)(1r‘𝑟)))}) |
31 | 9, 20, 30 | 3eqtrd 2834 | . . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → (ℤring(Hom ‘𝐶)𝑟) = {(𝑧 ∈ ℤ ↦ (𝑧(.g‘𝑟)(1r‘𝑟)))}) |
32 | sneq 4484 | . . . . . . 7 ⊢ (𝑓 = (𝑧 ∈ ℤ ↦ (𝑧(.g‘𝑟)(1r‘𝑟))) → {𝑓} = {(𝑧 ∈ ℤ ↦ (𝑧(.g‘𝑟)(1r‘𝑟)))}) | |
33 | 32 | eqeq2d 2804 | . . . . . 6 ⊢ (𝑓 = (𝑧 ∈ ℤ ↦ (𝑧(.g‘𝑟)(1r‘𝑟))) → ((ℤring(Hom ‘𝐶)𝑟) = {𝑓} ↔ (ℤring(Hom ‘𝐶)𝑟) = {(𝑧 ∈ ℤ ↦ (𝑧(.g‘𝑟)(1r‘𝑟)))})) |
34 | 33 | spcegv 3538 | . . . . 5 ⊢ ((𝑧 ∈ ℤ ↦ (𝑧(.g‘𝑟)(1r‘𝑟))) ∈ V → ((ℤring(Hom ‘𝐶)𝑟) = {(𝑧 ∈ ℤ ↦ (𝑧(.g‘𝑟)(1r‘𝑟)))} → ∃𝑓(ℤring(Hom ‘𝐶)𝑟) = {𝑓})) |
35 | 2, 31, 34 | mpsyl 68 | . . . 4 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → ∃𝑓(ℤring(Hom ‘𝐶)𝑟) = {𝑓}) |
36 | eusn 4575 | . . . 4 ⊢ (∃!𝑓 𝑓 ∈ (ℤring(Hom ‘𝐶)𝑟) ↔ ∃𝑓(ℤring(Hom ‘𝐶)𝑟) = {𝑓}) | |
37 | 35, 36 | sylibr 235 | . . 3 ⊢ ((𝜑 ∧ 𝑟 ∈ (Base‘𝐶)) → ∃!𝑓 𝑓 ∈ (ℤring(Hom ‘𝐶)𝑟)) |
38 | 37 | ralrimiva 3148 | . 2 ⊢ (𝜑 → ∀𝑟 ∈ (Base‘𝐶)∃!𝑓 𝑓 ∈ (ℤring(Hom ‘𝐶)𝑟)) |
39 | 3 | ringccat 43787 | . . . 4 ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) |
40 | 5, 39 | syl 17 | . . 3 ⊢ (𝜑 → 𝐶 ∈ Cat) |
41 | 12 | a1i 11 | . . . . 5 ⊢ (𝜑 → ℤring ∈ Ring) |
42 | 10, 41 | elind 4094 | . . . 4 ⊢ (𝜑 → ℤring ∈ (𝑈 ∩ Ring)) |
43 | 42, 16 | eleqtrrd 2885 | . . 3 ⊢ (𝜑 → ℤring ∈ (Base‘𝐶)) |
44 | 4, 6, 40, 43 | isinito 17089 | . 2 ⊢ (𝜑 → (ℤring ∈ (InitO‘𝐶) ↔ ∀𝑟 ∈ (Base‘𝐶)∃!𝑓 𝑓 ∈ (ℤring(Hom ‘𝐶)𝑟))) |
45 | 38, 44 | mpbird 258 | 1 ⊢ (𝜑 → ℤring ∈ (InitO‘𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∃wex 1762 ∈ wcel 2080 ∃!weu 2610 ∀wral 3104 Vcvv 3436 ∩ cin 3860 {csn 4474 ↦ cmpt 5043 × cxp 5444 ↾ cres 5448 ‘cfv 6228 (class class class)co 7019 ℤcz 11831 Basecbs 16312 Hom chom 16405 Catccat 16764 InitOcinito 17077 .gcmg 17981 1rcur 18941 Ringcrg 18987 RingHom crh 19154 ℤringzring 20299 RingCatcringc 43766 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-13 2343 ax-ext 2768 ax-rep 5084 ax-sep 5097 ax-nul 5104 ax-pow 5160 ax-pr 5224 ax-un 7322 ax-cnex 10442 ax-resscn 10443 ax-1cn 10444 ax-icn 10445 ax-addcl 10446 ax-addrcl 10447 ax-mulcl 10448 ax-mulrcl 10449 ax-mulcom 10450 ax-addass 10451 ax-mulass 10452 ax-distr 10453 ax-i2m1 10454 ax-1ne0 10455 ax-1rid 10456 ax-rnegex 10457 ax-rrecex 10458 ax-cnre 10459 ax-pre-lttri 10460 ax-pre-lttrn 10461 ax-pre-ltadd 10462 ax-pre-mulgt0 10463 ax-addf 10465 ax-mulf 10466 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1525 df-fal 1535 df-ex 1763 df-nf 1767 df-sb 2042 df-mo 2575 df-eu 2611 df-clab 2775 df-cleq 2787 df-clel 2862 df-nfc 2934 df-ne 2984 df-nel 3090 df-ral 3109 df-rex 3110 df-reu 3111 df-rmo 3112 df-rab 3113 df-v 3438 df-sbc 3708 df-csb 3814 df-dif 3864 df-un 3866 df-in 3868 df-ss 3876 df-pss 3878 df-nul 4214 df-if 4384 df-pw 4457 df-sn 4475 df-pr 4477 df-tp 4479 df-op 4481 df-uni 4748 df-int 4785 df-iun 4829 df-br 4965 df-opab 5027 df-mpt 5044 df-tr 5067 df-id 5351 df-eprel 5356 df-po 5365 df-so 5366 df-fr 5405 df-we 5407 df-xp 5452 df-rel 5453 df-cnv 5454 df-co 5455 df-dm 5456 df-rn 5457 df-res 5458 df-ima 5459 df-pred 6026 df-ord 6072 df-on 6073 df-lim 6074 df-suc 6075 df-iota 6192 df-fun 6230 df-fn 6231 df-f 6232 df-f1 6233 df-fo 6234 df-f1o 6235 df-fv 6236 df-riota 6980 df-ov 7022 df-oprab 7023 df-mpo 7024 df-om 7440 df-1st 7548 df-2nd 7549 df-wrecs 7801 df-recs 7863 df-rdg 7901 df-1o 7956 df-oadd 7960 df-er 8142 df-map 8261 df-pm 8262 df-ixp 8314 df-en 8361 df-dom 8362 df-sdom 8363 df-fin 8364 df-pnf 10526 df-mnf 10527 df-xr 10528 df-ltxr 10529 df-le 10530 df-sub 10721 df-neg 10722 df-nn 11489 df-2 11550 df-3 11551 df-4 11552 df-5 11553 df-6 11554 df-7 11555 df-8 11556 df-9 11557 df-n0 11748 df-z 11832 df-dec 11949 df-uz 12094 df-fz 12743 df-seq 13220 df-struct 16314 df-ndx 16315 df-slot 16316 df-base 16318 df-sets 16319 df-ress 16320 df-plusg 16407 df-mulr 16408 df-starv 16409 df-tset 16413 df-ple 16414 df-ds 16416 df-unif 16417 df-hom 16418 df-cco 16419 df-0g 16544 df-cat 16768 df-cid 16769 df-homf 16770 df-ssc 16909 df-resc 16910 df-subc 16911 df-inito 17080 df-estrc 17202 df-mgm 17681 df-sgrp 17723 df-mnd 17734 df-mhm 17774 df-grp 17864 df-minusg 17865 df-mulg 17982 df-subg 18030 df-ghm 18097 df-cmn 18635 df-mgp 18930 df-ur 18942 df-ring 18989 df-cring 18990 df-rnghom 19157 df-subrg 19223 df-cnfld 20228 df-zring 20300 df-ringc 43768 |
This theorem is referenced by: nzerooringczr 43835 |
Copyright terms: Public domain | W3C validator |