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 33339

Description: Ring localization is a proper operator, so it can be used with ovprc1 7397. (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 33338	. 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 7492	1 ⊢ Rel dom RLocal

Colors of variables: wff setvar class

Syntax hints: ∧ wa 395 ∈ wcel 2113 Vcvv 3440 ⦋csb 3849 ∪ cun 3899 ∅c0 4285 {ctp 4584 ⟨cop 4586 class class class wbr 5098 {copab 5160 × cxp 5622 dom cdm 5624 Rel wrel 5629 ‘cfv 6492 (class class class)co 7358 ∈ cmpo 7360 1^st c1st 7931 2^nd c2nd 7932 ndxcnx 17120 Basecbs 17136 +_gcplusg 17177 ._rcmulr 17178 Scalarcsca 17180 ·_𝑠 cvsca 17181 ·_𝑖cip 17182 TopSetcts 17183 lecple 17184 distcds 17186 ↾_t crest 17340 /_s cqus 17426 ×_t ctx 23504 ~_RL cerl 33335 RLocal crloc 33336

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-sep 5241 ax-nul 5251 ax-pr 5377

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-rab 3400 df-v 3442 df-dif 3904 df-un 3906 df-ss 3918 df-nul 4286 df-if 4480 df-sn 4581 df-pr 4583 df-op 4587 df-br 5099 df-opab 5161 df-xp 5630 df-rel 5631 df-dm 5634 df-oprab 7362 df-mpo 7363 df-rloc 33338

This theorem is referenced by: fracval 33386

W3C validator