ringciso - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ringciso		Structured version Visualization version GIF version

Theorem ringciso 20757

Description: An isomorphism in the category of unital rings is a bijection. (Contributed by AV, 14-Feb-2020.)

**Hypotheses**
Ref	Expression
ringcsect.c	⊢ 𝐶 = (RingCat‘𝑈)
ringcsect.b	⊢ 𝐵 = (Base‘𝐶)
ringcsect.u	⊢ (𝜑 → 𝑈 ∈ 𝑉)
ringcsect.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
ringcsect.y	⊢ (𝜑 → 𝑌 ∈ 𝐵)
ringciso.n	⊢ 𝐼 = (Iso‘𝐶)

**Assertion**
Ref	Expression
ringciso	⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RingIso 𝑌)))

**Proof of Theorem ringciso**
Step	Hyp	Ref	Expression
1		ringcsect.b	. . . 4 ⊢ 𝐵 = (Base‘𝐶)
2		eqid 2769	. . . 4 ⊢ (Inv‘𝐶) = (Inv‘𝐶)
3		ringcsect.u	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ 𝑉)
4		ringcsect.c	. . . . . 6 ⊢ 𝐶 = (RingCat‘𝑈)
5	4	ringccat 20748	. . . . 5 ⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat)
6	3, 5	syl 18	. . . 4 ⊢ (𝜑 → 𝐶 ∈ Cat)
7		ringcsect.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
8		ringcsect.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝐵)
9		ringciso.n	. . . 4 ⊢ 𝐼 = (Iso‘𝐶)
10	1, 2, 6, 7, 8, 9	isoval 17822	. . 3 ⊢ (𝜑 → (𝑋𝐼𝑌) = dom (𝑋(Inv‘𝐶)𝑌))
11	10	eleq2d 2855	. 2 ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌)))
12	1, 2, 6, 7, 8	invfun 17821	. . . . 5 ⊢ (𝜑 → Fun (𝑋(Inv‘𝐶)𝑌))
13		funfvbrb 7047	. . . . 5 ⊢ (Fun (𝑋(Inv‘𝐶)𝑌) → (𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌) ↔ 𝐹(𝑋(Inv‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)))
14	12, 13	syl 18	. . . 4 ⊢ (𝜑 → (𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌) ↔ 𝐹(𝑋(Inv‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)))
15	4, 1, 3, 7, 8, 2	ringcinv 20756	. . . . 5 ⊢ (𝜑 → (𝐹(𝑋(Inv‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹) ↔ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ ((𝑋(Inv‘𝐶)𝑌)‘𝐹) = ^◡𝐹)))
16		simpl 487	. . . . 5 ⊢ ((𝐹 ∈ (𝑋 RingIso 𝑌) ∧ ((𝑋(Inv‘𝐶)𝑌)‘𝐹) = ^◡𝐹) → 𝐹 ∈ (𝑋 RingIso 𝑌))
17	15, 16	biimtrdi 256	. . . 4 ⊢ (𝜑 → (𝐹(𝑋(Inv‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹) → 𝐹 ∈ (𝑋 RingIso 𝑌)))
18	14, 17	sylbid 243	. . 3 ⊢ (𝜑 → (𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌) → 𝐹 ∈ (𝑋 RingIso 𝑌)))
19		eqid 2769	. . . 4 ⊢ ^◡𝐹 = ^◡𝐹
20	4, 1, 3, 7, 8, 2	ringcinv 20756	. . . . 5 ⊢ (𝜑 → (𝐹(𝑋(Inv‘𝐶)𝑌)^◡𝐹 ↔ (𝐹 ∈ (𝑋 RingIso 𝑌) ∧ ^◡𝐹 = ^◡𝐹)))
21		funrel 6554	. . . . . . 7 ⊢ (Fun (𝑋(Inv‘𝐶)𝑌) → Rel (𝑋(Inv‘𝐶)𝑌))
22	12, 21	syl 18	. . . . . 6 ⊢ (𝜑 → Rel (𝑋(Inv‘𝐶)𝑌))
23		releldm 5935	. . . . . . 7 ⊢ ((Rel (𝑋(Inv‘𝐶)𝑌) ∧ 𝐹(𝑋(Inv‘𝐶)𝑌)^◡𝐹) → 𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌))
24	23	ex 417	. . . . . 6 ⊢ (Rel (𝑋(Inv‘𝐶)𝑌) → (𝐹(𝑋(Inv‘𝐶)𝑌)^◡𝐹 → 𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌)))
25	22, 24	syl 18	. . . . 5 ⊢ (𝜑 → (𝐹(𝑋(Inv‘𝐶)𝑌)^◡𝐹 → 𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌)))
26	20, 25	sylbird 263	. . . 4 ⊢ (𝜑 → ((𝐹 ∈ (𝑋 RingIso 𝑌) ∧ ^◡𝐹 = ^◡𝐹) → 𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌)))
27	19, 26	mpan2i 709	. . 3 ⊢ (𝜑 → (𝐹 ∈ (𝑋 RingIso 𝑌) → 𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌)))
28	18, 27	impbid 215	. 2 ⊢ (𝜑 → (𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌) ↔ 𝐹 ∈ (𝑋 RingIso 𝑌)))
29	11, 28	bitrd 282	1 ⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ (𝑋 RingIso 𝑌)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1567 ∈ wcel 2149 class class class wbr 5111 ^◡ccnv 5661 dom cdm 5662 Rel wrel 5667 Fun wfun 6531 ‘cfv 6537 (class class class)co 7411 Basecbs 17269 Catccat 17720 Invcinv 17802 Isociso 17803 RingIso crs 20552 RingCatcringc 20730

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3375 df-reu 3376 df-rab 3423 df-v 3463 df-sbc 3752 df-csb 3860 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3931 df-nul 4293 df-if 4491 df-pw 4567 df-sn 4593 df-pr 4595 df-tp 4597 df-op 4599 df-uni 4875 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-er 8694 df-map 8826 df-pm 8827 df-ixp 8896 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12505 df-z 12592 df-dec 12712 df-uz 12863 df-fz 13536 df-struct 17207 df-sets 17224 df-slot 17242 df-ndx 17254 df-base 17270 df-ress 17291 df-plusg 17323 df-hom 17334 df-cco 17335 df-0g 17494 df-cat 17724 df-cid 17725 df-homf 17726 df-sect 17804 df-inv 17805 df-iso 17806 df-ssc 17867 df-resc 17868 df-subc 17869 df-estrc 18179 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-mhm 18841 df-grp 19003 df-ghm 19284 df-mgp 20217 df-ur 20264 df-ring 20317 df-rhm 20554 df-rim 20555 df-ringc 20731

This theorem is referenced by: (None)

W3C validator