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 33577

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

Colors of variables: wff setvar class

Syntax hints: ∧ wa 400 ∈ wcel 2143 Vcvv 3455 ⦋csb 3853 ∪ cun 3903 ∅c0 4286 {ctp 4593 ⟨cop 4595 class class class wbr 5109 {copab 5173 × cxp 5659 dom cdm 5661 Rel wrel 5666 ‘cfv 6536 (class class class)co 7410 ∈ cmpo 7412 1^st c1st 7980 2^nd c2nd 7981 ndxcnx 17248 Basecbs 17264 +_gcplusg 17305 ._rcmulr 17306 Scalarcsca 17308 ·_𝑠 cvsca 17309 ·_𝑖cip 17310 TopSetcts 17311 lecple 17312 distcds 17314 ↾_t crest 17468 /_s cqus 17554 ×_t ctx 23717 ~_RL cerl 33573 RLocal crloc 33574

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-pr 5404

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-rab 3417 df-v 3457 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-nul 4287 df-if 4488 df-sn 4590 df-pr 4592 df-op 4596 df-br 5110 df-opab 5174 df-xp 5667 df-rel 5668 df-dm 5671 df-oprab 7414 df-mpo 7415 df-rloc 33576

This theorem is referenced by: fracval 33625

W3C validator