reldmrloc - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > reldmrloc		Structured version Visualization version GIF version

Theorem reldmrloc 33200

Description: Ring localization is a proper operator, so it can be used with ovprc1 7452. (Contributed by Thierry Arnoux, 10-May-2025.)

**Assertion**
Ref	Expression
reldmrloc	⊢ Rel dom RLocal

Proof of Theorem reldmrloc Dummy variables 𝑎 𝑏 𝑘 𝑟 𝑠 𝑤 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-rloc 33199	. 2 ⊢ RLocal = (𝑟 ∈ V, 𝑠 ∈ V ↦ ⦋(._r‘𝑟) / 𝑥⦌⦋((Base‘𝑟) × 𝑠) / 𝑤⦌((({⟨(Base‘ndx), 𝑤⟩, ⟨(+_g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨(((1^st ‘𝑎)𝑥(2^nd ‘𝑏))(+_g‘𝑟)((1^st ‘𝑏)𝑥(2^nd ‘𝑎))), ((2^nd ‘𝑎)𝑥(2^nd ‘𝑏))⟩)⟩, ⟨(._r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ ⟨((1^st ‘𝑎)𝑥(1^st ‘𝑏)), ((2^nd ‘𝑎)𝑥(2^nd ‘𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·_𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ ⟨(𝑘( ·_𝑠 ‘𝑟)(1^st ‘𝑎)), (2^nd ‘𝑎)⟩)⟩, ⟨(·_𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×_t ((TopSet‘𝑟) ↾_t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1^st ‘𝑎)𝑥(2^nd ‘𝑏))(le‘𝑟)((1^st ‘𝑏)𝑥(2^nd ‘𝑎)))}⟩, ⟨(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1^st ‘𝑎)𝑥(2^nd ‘𝑏))(dist‘𝑟)((1^st ‘𝑏)𝑥(2^nd ‘𝑎))))⟩}) /_s (𝑟 ~_RL 𝑠)))
2	1	reldmmpo 7549	1 ⊢ Rel dom RLocal

Colors of variables: wff setvar class

Syntax hints: ∧ wa 395 ∈ wcel 2107 Vcvv 3463 ⦋csb 3879 ∪ cun 3929 ∅c0 4313 {ctp 4610 ⟨cop 4612 class class class wbr 5123 {copab 5185 × cxp 5663 dom cdm 5665 Rel wrel 5670 ‘cfv 6541 (class class class)co 7413 ∈ cmpo 7415 1^st c1st 7994 2^nd c2nd 7995 ndxcnx 17212 Basecbs 17229 +_gcplusg 17273 ._rcmulr 17274 Scalarcsca 17276 ·_𝑠 cvsca 17277 ·_𝑖cip 17278 TopSetcts 17279 lecple 17280 distcds 17282 ↾_t crest 17436 /_s cqus 17521 ×_t ctx 23514 ~_RL cerl 33196 RLocal crloc 33197

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-sep 5276 ax-nul 5286 ax-pr 5412

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-rab 3420 df-v 3465 df-dif 3934 df-un 3936 df-ss 3948 df-nul 4314 df-if 4506 df-sn 4607 df-pr 4609 df-op 4613 df-br 5124 df-opab 5186 df-xp 5671 df-rel 5672 df-dm 5675 df-oprab 7417 df-mpo 7418 df-rloc 33199

This theorem is referenced by: fracval 33246

W3C validator