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

Theorem rlocval 33246
Description: Expand the value of the ring localization operation. (Contributed by Thierry Arnoux, 4-May-2025.)
Hypotheses
Ref Expression
rlocval.1 𝐵 = (Base‘𝑅)
rlocval.2 0 = (0g𝑅)
rlocval.3 · = (.r𝑅)
rlocval.4 = (-g𝑅)
rlocval.5 + = (+g𝑅)
rlocval.6 = (le‘𝑅)
rlocval.7 𝐹 = (Scalar‘𝑅)
rlocval.8 𝐾 = (Base‘𝐹)
rlocval.9 𝐶 = ( ·𝑠𝑅)
rlocval.10 𝑊 = (𝐵 × 𝑆)
rlocval.11 = (𝑅 ~RL 𝑆)
rlocval.12 𝐽 = (TopSet‘𝑅)
rlocval.13 𝐷 = (dist‘𝑅)
rlocval.14 = (𝑎𝑊, 𝑏𝑊 ↦ ⟨(((1st𝑎) · (2nd𝑏)) + ((1st𝑏) · (2nd𝑎))), ((2nd𝑎) · (2nd𝑏))⟩)
rlocval.15 = (𝑎𝑊, 𝑏𝑊 ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)
rlocval.16 × = (𝑘𝐾, 𝑎𝑊 ↦ ⟨(𝑘𝐶(1st𝑎)), (2nd𝑎)⟩)
rlocval.17 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))}
rlocval.18 𝐸 = (𝑎𝑊, 𝑏𝑊 ↦ (((1st𝑎) · (2nd𝑏))𝐷((1st𝑏) · (2nd𝑎))))
rlocval.19 (𝜑𝑅𝑉)
rlocval.20 (𝜑𝑆𝐵)
Assertion
Ref Expression
rlocval (𝜑 → (𝑅 RLocal 𝑆) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽t 𝑆))⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ))
Distinct variable groups:   · ,𝑎,𝑏,𝑘   𝑅,𝑎,𝑏,𝑘   𝑆,𝑎,𝑏,𝑘   𝑊,𝑎,𝑏,𝑘
Allowed substitution hints:   𝜑(𝑘,𝑎,𝑏)   𝐵(𝑘,𝑎,𝑏)   𝐶(𝑘,𝑎,𝑏)   𝐷(𝑘,𝑎,𝑏)   + (𝑘,𝑎,𝑏)   (𝑘,𝑎,𝑏)   (𝑘,𝑎,𝑏)   × (𝑘,𝑎,𝑏)   (𝑘,𝑎,𝑏)   𝐸(𝑘,𝑎,𝑏)   𝐹(𝑘,𝑎,𝑏)   𝐽(𝑘,𝑎,𝑏)   𝐾(𝑘,𝑎,𝑏)   (𝑘,𝑎,𝑏)   (𝑘,𝑎,𝑏)   𝑉(𝑘,𝑎,𝑏)   0 (𝑘,𝑎,𝑏)   (𝑘,𝑎,𝑏)

Proof of Theorem rlocval
Dummy variables 𝑟 𝑠 𝑤 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rlocval.19 . . 3 (𝜑𝑅𝑉)
21elexd 3502 . 2 (𝜑𝑅 ∈ V)
3 rlocval.1 . . . . 5 𝐵 = (Base‘𝑅)
43fvexi 6921 . . . 4 𝐵 ∈ V
54a1i 11 . . 3 (𝜑𝐵 ∈ V)
6 rlocval.20 . . 3 (𝜑𝑆𝐵)
75, 6ssexd 5330 . 2 (𝜑𝑆 ∈ V)
8 ovexd 7466 . 2 (𝜑 → ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽t 𝑆))⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ) ∈ V)
9 fvexd 6922 . . . 4 ((𝑟 = 𝑅𝑠 = 𝑆) → (.r𝑟) ∈ V)
10 fveq2 6907 . . . . . 6 (𝑟 = 𝑅 → (.r𝑟) = (.r𝑅))
1110adantr 480 . . . . 5 ((𝑟 = 𝑅𝑠 = 𝑆) → (.r𝑟) = (.r𝑅))
12 rlocval.3 . . . . 5 · = (.r𝑅)
1311, 12eqtr4di 2793 . . . 4 ((𝑟 = 𝑅𝑠 = 𝑆) → (.r𝑟) = · )
14 fvexd 6922 . . . . . 6 (((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) → (Base‘𝑟) ∈ V)
15 vex 3482 . . . . . . 7 𝑠 ∈ V
1615a1i 11 . . . . . 6 (((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) → 𝑠 ∈ V)
1714, 16xpexd 7770 . . . . 5 (((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) → ((Base‘𝑟) × 𝑠) ∈ V)
18 fveq2 6907 . . . . . . . . 9 (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅))
1918ad2antrr 726 . . . . . . . 8 (((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) → (Base‘𝑟) = (Base‘𝑅))
2019, 3eqtr4di 2793 . . . . . . 7 (((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) → (Base‘𝑟) = 𝐵)
21 simplr 769 . . . . . . 7 (((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) → 𝑠 = 𝑆)
2220, 21xpeq12d 5720 . . . . . 6 (((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) → ((Base‘𝑟) × 𝑠) = (𝐵 × 𝑆))
23 rlocval.10 . . . . . 6 𝑊 = (𝐵 × 𝑆)
2422, 23eqtr4di 2793 . . . . 5 (((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) → ((Base‘𝑟) × 𝑠) = 𝑊)
25 simpr 484 . . . . . . . . . 10 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑤 = 𝑊)
2625opeq2d 4885 . . . . . . . . 9 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(Base‘ndx), 𝑤⟩ = ⟨(Base‘ndx), 𝑊⟩)
27 simplll 775 . . . . . . . . . . . . . . . 16 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑟 = 𝑅)
2827fveq2d 6911 . . . . . . . . . . . . . . 15 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (+g𝑟) = (+g𝑅))
29 rlocval.5 . . . . . . . . . . . . . . 15 + = (+g𝑅)
3028, 29eqtr4di 2793 . . . . . . . . . . . . . 14 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (+g𝑟) = + )
31 simplr 769 . . . . . . . . . . . . . . 15 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑥 = · )
3231oveqd 7448 . . . . . . . . . . . . . 14 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st𝑎)𝑥(2nd𝑏)) = ((1st𝑎) · (2nd𝑏)))
3331oveqd 7448 . . . . . . . . . . . . . 14 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st𝑏)𝑥(2nd𝑎)) = ((1st𝑏) · (2nd𝑎)))
3430, 32, 33oveq123d 7452 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st𝑎)𝑥(2nd𝑏))(+g𝑟)((1st𝑏)𝑥(2nd𝑎))) = (((1st𝑎) · (2nd𝑏)) + ((1st𝑏) · (2nd𝑎))))
3531oveqd 7448 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((2nd𝑎)𝑥(2nd𝑏)) = ((2nd𝑎) · (2nd𝑏)))
3634, 35opeq12d 4886 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(((1st𝑎)𝑥(2nd𝑏))(+g𝑟)((1st𝑏)𝑥(2nd𝑎))), ((2nd𝑎)𝑥(2nd𝑏))⟩ = ⟨(((1st𝑎) · (2nd𝑏)) + ((1st𝑏) · (2nd𝑎))), ((2nd𝑎) · (2nd𝑏))⟩)
3725, 25, 36mpoeq123dv 7508 . . . . . . . . . . 11 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎𝑤, 𝑏𝑤 ↦ ⟨(((1st𝑎)𝑥(2nd𝑏))(+g𝑟)((1st𝑏)𝑥(2nd𝑎))), ((2nd𝑎)𝑥(2nd𝑏))⟩) = (𝑎𝑊, 𝑏𝑊 ↦ ⟨(((1st𝑎) · (2nd𝑏)) + ((1st𝑏) · (2nd𝑎))), ((2nd𝑎) · (2nd𝑏))⟩))
38 rlocval.14 . . . . . . . . . . 11 = (𝑎𝑊, 𝑏𝑊 ↦ ⟨(((1st𝑎) · (2nd𝑏)) + ((1st𝑏) · (2nd𝑎))), ((2nd𝑎) · (2nd𝑏))⟩)
3937, 38eqtr4di 2793 . . . . . . . . . 10 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎𝑤, 𝑏𝑤 ↦ ⟨(((1st𝑎)𝑥(2nd𝑏))(+g𝑟)((1st𝑏)𝑥(2nd𝑎))), ((2nd𝑎)𝑥(2nd𝑏))⟩) = )
4039opeq2d 4885 . . . . . . . . 9 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(+g‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨(((1st𝑎)𝑥(2nd𝑏))(+g𝑟)((1st𝑏)𝑥(2nd𝑎))), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩ = ⟨(+g‘ndx), ⟩)
4131oveqd 7448 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st𝑎)𝑥(1st𝑏)) = ((1st𝑎) · (1st𝑏)))
4241, 35opeq12d 4886 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨((1st𝑎)𝑥(1st𝑏)), ((2nd𝑎)𝑥(2nd𝑏))⟩ = ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)
4325, 25, 42mpoeq123dv 7508 . . . . . . . . . . 11 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎𝑤, 𝑏𝑤 ↦ ⟨((1st𝑎)𝑥(1st𝑏)), ((2nd𝑎)𝑥(2nd𝑏))⟩) = (𝑎𝑊, 𝑏𝑊 ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩))
44 rlocval.15 . . . . . . . . . . 11 = (𝑎𝑊, 𝑏𝑊 ↦ ⟨((1st𝑎) · (1st𝑏)), ((2nd𝑎) · (2nd𝑏))⟩)
4543, 44eqtr4di 2793 . . . . . . . . . 10 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎𝑤, 𝑏𝑤 ↦ ⟨((1st𝑎)𝑥(1st𝑏)), ((2nd𝑎)𝑥(2nd𝑏))⟩) = )
4645opeq2d 4885 . . . . . . . . 9 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(.r‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨((1st𝑎)𝑥(1st𝑏)), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩ = ⟨(.r‘ndx), ⟩)
4726, 40, 46tpeq123d 4753 . . . . . . . 8 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨(((1st𝑎)𝑥(2nd𝑏))(+g𝑟)((1st𝑏)𝑥(2nd𝑎))), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨((1st𝑎)𝑥(1st𝑏)), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩} = {⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩})
4827fveq2d 6911 . . . . . . . . . . 11 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Scalar‘𝑟) = (Scalar‘𝑅))
49 rlocval.7 . . . . . . . . . . 11 𝐹 = (Scalar‘𝑅)
5048, 49eqtr4di 2793 . . . . . . . . . 10 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Scalar‘𝑟) = 𝐹)
5150opeq2d 4885 . . . . . . . . 9 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(Scalar‘ndx), (Scalar‘𝑟)⟩ = ⟨(Scalar‘ndx), 𝐹⟩)
5248fveq2d 6911 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Base‘(Scalar‘𝑟)) = (Base‘(Scalar‘𝑅)))
53 rlocval.8 . . . . . . . . . . . . . 14 𝐾 = (Base‘𝐹)
5449fveq2i 6910 . . . . . . . . . . . . . 14 (Base‘𝐹) = (Base‘(Scalar‘𝑅))
5553, 54eqtri 2763 . . . . . . . . . . . . 13 𝐾 = (Base‘(Scalar‘𝑅))
5652, 55eqtr4di 2793 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Base‘(Scalar‘𝑟)) = 𝐾)
5727fveq2d 6911 . . . . . . . . . . . . . . 15 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ( ·𝑠𝑟) = ( ·𝑠𝑅))
58 rlocval.9 . . . . . . . . . . . . . . 15 𝐶 = ( ·𝑠𝑅)
5957, 58eqtr4di 2793 . . . . . . . . . . . . . 14 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ( ·𝑠𝑟) = 𝐶)
6059oveqd 7448 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑘( ·𝑠𝑟)(1st𝑎)) = (𝑘𝐶(1st𝑎)))
6160opeq1d 4884 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(𝑘( ·𝑠𝑟)(1st𝑎)), (2nd𝑎)⟩ = ⟨(𝑘𝐶(1st𝑎)), (2nd𝑎)⟩)
6256, 25, 61mpoeq123dv 7508 . . . . . . . . . . 11 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎𝑤 ↦ ⟨(𝑘( ·𝑠𝑟)(1st𝑎)), (2nd𝑎)⟩) = (𝑘𝐾, 𝑎𝑊 ↦ ⟨(𝑘𝐶(1st𝑎)), (2nd𝑎)⟩))
63 rlocval.16 . . . . . . . . . . 11 × = (𝑘𝐾, 𝑎𝑊 ↦ ⟨(𝑘𝐶(1st𝑎)), (2nd𝑎)⟩)
6462, 63eqtr4di 2793 . . . . . . . . . 10 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎𝑤 ↦ ⟨(𝑘( ·𝑠𝑟)(1st𝑎)), (2nd𝑎)⟩) = × )
6564opeq2d 4885 . . . . . . . . 9 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎𝑤 ↦ ⟨(𝑘( ·𝑠𝑟)(1st𝑎)), (2nd𝑎)⟩)⟩ = ⟨( ·𝑠 ‘ndx), × ⟩)
66 eqidd 2736 . . . . . . . . 9 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(·𝑖‘ndx), ∅⟩ = ⟨(·𝑖‘ndx), ∅⟩)
6751, 65, 66tpeq123d 4753 . . . . . . . 8 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎𝑤 ↦ ⟨(𝑘( ·𝑠𝑟)(1st𝑎)), (2nd𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩} = {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩})
6847, 67uneq12d 4179 . . . . . . 7 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨(((1st𝑎)𝑥(2nd𝑏))(+g𝑟)((1st𝑏)𝑥(2nd𝑎))), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨((1st𝑎)𝑥(1st𝑏)), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎𝑤 ↦ ⟨(𝑘( ·𝑠𝑟)(1st𝑎)), (2nd𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) = ({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}))
6927fveq2d 6911 . . . . . . . . . . 11 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (TopSet‘𝑟) = (TopSet‘𝑅))
70 rlocval.12 . . . . . . . . . . 11 𝐽 = (TopSet‘𝑅)
7169, 70eqtr4di 2793 . . . . . . . . . 10 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (TopSet‘𝑟) = 𝐽)
7221adantr 480 . . . . . . . . . . 11 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑠 = 𝑆)
7371, 72oveq12d 7449 . . . . . . . . . 10 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((TopSet‘𝑟) ↾t 𝑠) = (𝐽t 𝑆))
7471, 73oveq12d 7449 . . . . . . . . 9 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠)) = (𝐽 ×t (𝐽t 𝑆)))
7574opeq2d 4885 . . . . . . . 8 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩ = ⟨(TopSet‘ndx), (𝐽 ×t (𝐽t 𝑆))⟩)
7625eleq2d 2825 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎𝑤𝑎𝑊))
7725eleq2d 2825 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑏𝑤𝑏𝑊))
7876, 77anbi12d 632 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((𝑎𝑤𝑏𝑤) ↔ (𝑎𝑊𝑏𝑊)))
7927fveq2d 6911 . . . . . . . . . . . . . 14 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (le‘𝑟) = (le‘𝑅))
80 rlocval.6 . . . . . . . . . . . . . 14 = (le‘𝑅)
8179, 80eqtr4di 2793 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (le‘𝑟) = )
8232, 81, 33breq123d 5162 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st𝑎)𝑥(2nd𝑏))(le‘𝑟)((1st𝑏)𝑥(2nd𝑎)) ↔ ((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎))))
8378, 82anbi12d 632 . . . . . . . . . . 11 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((𝑎𝑤𝑏𝑤) ∧ ((1st𝑎)𝑥(2nd𝑏))(le‘𝑟)((1st𝑏)𝑥(2nd𝑎))) ↔ ((𝑎𝑊𝑏𝑊) ∧ ((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))))
8483opabbidv 5214 . . . . . . . . . 10 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑤𝑏𝑤) ∧ ((1st𝑎)𝑥(2nd𝑏))(le‘𝑟)((1st𝑏)𝑥(2nd𝑎)))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))})
85 rlocval.17 . . . . . . . . . 10 = {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑊𝑏𝑊) ∧ ((1st𝑎) · (2nd𝑏)) ((1st𝑏) · (2nd𝑎)))}
8684, 85eqtr4di 2793 . . . . . . . . 9 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑤𝑏𝑤) ∧ ((1st𝑎)𝑥(2nd𝑏))(le‘𝑟)((1st𝑏)𝑥(2nd𝑎)))} = )
8786opeq2d 4885 . . . . . . . 8 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑤𝑏𝑤) ∧ ((1st𝑎)𝑥(2nd𝑏))(le‘𝑟)((1st𝑏)𝑥(2nd𝑎)))}⟩ = ⟨(le‘ndx), ⟩)
8827fveq2d 6911 . . . . . . . . . . . . 13 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (dist‘𝑟) = (dist‘𝑅))
89 rlocval.13 . . . . . . . . . . . . 13 𝐷 = (dist‘𝑅)
9088, 89eqtr4di 2793 . . . . . . . . . . . 12 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (dist‘𝑟) = 𝐷)
9190, 32, 33oveq123d 7452 . . . . . . . . . . 11 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st𝑎)𝑥(2nd𝑏))(dist‘𝑟)((1st𝑏)𝑥(2nd𝑎))) = (((1st𝑎) · (2nd𝑏))𝐷((1st𝑏) · (2nd𝑎))))
9225, 25, 91mpoeq123dv 7508 . . . . . . . . . 10 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎𝑤, 𝑏𝑤 ↦ (((1st𝑎)𝑥(2nd𝑏))(dist‘𝑟)((1st𝑏)𝑥(2nd𝑎)))) = (𝑎𝑊, 𝑏𝑊 ↦ (((1st𝑎) · (2nd𝑏))𝐷((1st𝑏) · (2nd𝑎)))))
93 rlocval.18 . . . . . . . . . 10 𝐸 = (𝑎𝑊, 𝑏𝑊 ↦ (((1st𝑎) · (2nd𝑏))𝐷((1st𝑏) · (2nd𝑎))))
9492, 93eqtr4di 2793 . . . . . . . . 9 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎𝑤, 𝑏𝑤 ↦ (((1st𝑎)𝑥(2nd𝑏))(dist‘𝑟)((1st𝑏)𝑥(2nd𝑎)))) = 𝐸)
9594opeq2d 4885 . . . . . . . 8 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ⟨(dist‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ (((1st𝑎)𝑥(2nd𝑏))(dist‘𝑟)((1st𝑏)𝑥(2nd𝑎))))⟩ = ⟨(dist‘ndx), 𝐸⟩)
9675, 87, 95tpeq123d 4753 . . . . . . 7 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑤𝑏𝑤) ∧ ((1st𝑎)𝑥(2nd𝑏))(le‘𝑟)((1st𝑏)𝑥(2nd𝑎)))}⟩, ⟨(dist‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ (((1st𝑎)𝑥(2nd𝑏))(dist‘𝑟)((1st𝑏)𝑥(2nd𝑎))))⟩} = {⟨(TopSet‘ndx), (𝐽 ×t (𝐽t 𝑆))⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐸⟩})
9768, 96uneq12d 4179 . . . . . 6 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨(((1st𝑎)𝑥(2nd𝑏))(+g𝑟)((1st𝑏)𝑥(2nd𝑎))), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨((1st𝑎)𝑥(1st𝑏)), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎𝑤 ↦ ⟨(𝑘( ·𝑠𝑟)(1st𝑎)), (2nd𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑤𝑏𝑤) ∧ ((1st𝑎)𝑥(2nd𝑏))(le‘𝑟)((1st𝑏)𝑥(2nd𝑎)))}⟩, ⟨(dist‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ (((1st𝑎)𝑥(2nd𝑏))(dist‘𝑟)((1st𝑏)𝑥(2nd𝑎))))⟩}) = (({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽t 𝑆))⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐸⟩}))
9827, 72oveq12d 7449 . . . . . . 7 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑟 ~RL 𝑠) = (𝑅 ~RL 𝑆))
99 rlocval.11 . . . . . . 7 = (𝑅 ~RL 𝑆)
10098, 99eqtr4di 2793 . . . . . 6 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑟 ~RL 𝑠) = )
10197, 100oveq12d 7449 . . . . 5 ((((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨(((1st𝑎)𝑥(2nd𝑏))(+g𝑟)((1st𝑏)𝑥(2nd𝑎))), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨((1st𝑎)𝑥(1st𝑏)), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎𝑤 ↦ ⟨(𝑘( ·𝑠𝑟)(1st𝑎)), (2nd𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑤𝑏𝑤) ∧ ((1st𝑎)𝑥(2nd𝑏))(le‘𝑟)((1st𝑏)𝑥(2nd𝑎)))}⟩, ⟨(dist‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ (((1st𝑎)𝑥(2nd𝑏))(dist‘𝑟)((1st𝑏)𝑥(2nd𝑎))))⟩}) /s (𝑟 ~RL 𝑠)) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽t 𝑆))⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ))
10217, 24, 101csbied2 3948 . . . 4 (((𝑟 = 𝑅𝑠 = 𝑆) ∧ 𝑥 = · ) → ((Base‘𝑟) × 𝑠) / 𝑤((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨(((1st𝑎)𝑥(2nd𝑏))(+g𝑟)((1st𝑏)𝑥(2nd𝑎))), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨((1st𝑎)𝑥(1st𝑏)), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎𝑤 ↦ ⟨(𝑘( ·𝑠𝑟)(1st𝑎)), (2nd𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑤𝑏𝑤) ∧ ((1st𝑎)𝑥(2nd𝑏))(le‘𝑟)((1st𝑏)𝑥(2nd𝑎)))}⟩, ⟨(dist‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ (((1st𝑎)𝑥(2nd𝑏))(dist‘𝑟)((1st𝑏)𝑥(2nd𝑎))))⟩}) /s (𝑟 ~RL 𝑠)) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽t 𝑆))⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ))
1039, 13, 102csbied2 3948 . . 3 ((𝑟 = 𝑅𝑠 = 𝑆) → (.r𝑟) / 𝑥((Base‘𝑟) × 𝑠) / 𝑤((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨(((1st𝑎)𝑥(2nd𝑏))(+g𝑟)((1st𝑏)𝑥(2nd𝑎))), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨((1st𝑎)𝑥(1st𝑏)), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎𝑤 ↦ ⟨(𝑘( ·𝑠𝑟)(1st𝑎)), (2nd𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑤𝑏𝑤) ∧ ((1st𝑎)𝑥(2nd𝑏))(le‘𝑟)((1st𝑏)𝑥(2nd𝑎)))}⟩, ⟨(dist‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ (((1st𝑎)𝑥(2nd𝑏))(dist‘𝑟)((1st𝑏)𝑥(2nd𝑎))))⟩}) /s (𝑟 ~RL 𝑠)) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽t 𝑆))⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ))
104 df-rloc 33243 . . 3 RLocal = (𝑟 ∈ V, 𝑠 ∈ V ↦ (.r𝑟) / 𝑥((Base‘𝑟) × 𝑠) / 𝑤((({⟨(Base‘ndx), 𝑤⟩, ⟨(+g‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨(((1st𝑎)𝑥(2nd𝑏))(+g𝑟)((1st𝑏)𝑥(2nd𝑎))), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩, ⟨(.r‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ ⟨((1st𝑎)𝑥(1st𝑏)), ((2nd𝑎)𝑥(2nd𝑏))⟩)⟩} ∪ {⟨(Scalar‘ndx), (Scalar‘𝑟)⟩, ⟨( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎𝑤 ↦ ⟨(𝑘( ·𝑠𝑟)(1st𝑎)), (2nd𝑎)⟩)⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠))⟩, ⟨(le‘ndx), {⟨𝑎, 𝑏⟩ ∣ ((𝑎𝑤𝑏𝑤) ∧ ((1st𝑎)𝑥(2nd𝑏))(le‘𝑟)((1st𝑏)𝑥(2nd𝑎)))}⟩, ⟨(dist‘ndx), (𝑎𝑤, 𝑏𝑤 ↦ (((1st𝑎)𝑥(2nd𝑏))(dist‘𝑟)((1st𝑏)𝑥(2nd𝑎))))⟩}) /s (𝑟 ~RL 𝑠)))
105103, 104ovmpoga 7587 . 2 ((𝑅 ∈ V ∧ 𝑆 ∈ V ∧ ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽t 𝑆))⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ) ∈ V) → (𝑅 RLocal 𝑆) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽t 𝑆))⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ))
1062, 7, 8, 105syl3anc 1370 1 (𝜑 → (𝑅 RLocal 𝑆) = ((({⟨(Base‘ndx), 𝑊⟩, ⟨(+g‘ndx), ⟩, ⟨(.r‘ndx), ⟩} ∪ {⟨(Scalar‘ndx), 𝐹⟩, ⟨( ·𝑠 ‘ndx), × ⟩, ⟨(·𝑖‘ndx), ∅⟩}) ∪ {⟨(TopSet‘ndx), (𝐽 ×t (𝐽t 𝑆))⟩, ⟨(le‘ndx), ⟩, ⟨(dist‘ndx), 𝐸⟩}) /s ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2106  Vcvv 3478  csb 3908  cun 3961  wss 3963  c0 4339  {ctp 4635  cop 4637   class class class wbr 5148  {copab 5210   × cxp 5687  cfv 6563  (class class class)co 7431  cmpo 7433  1st c1st 8011  2nd c2nd 8012  ndxcnx 17227  Basecbs 17245  +gcplusg 17298  .rcmulr 17299  Scalarcsca 17301   ·𝑠 cvsca 17302  ·𝑖cip 17303  TopSetcts 17304  lecple 17305  distcds 17307  t crest 17467  0gc0g 17486   /s cqus 17552  -gcsg 18966   ×t ctx 23584   ~RL cerl 33240   RLocal crloc 33241
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-iota 6516  df-fun 6565  df-fv 6571  df-ov 7434  df-oprab 7435  df-mpo 7436  df-rloc 33243
This theorem is referenced by:  rlocbas  33254  rlocaddval  33255  rlocmulval  33256
  Copyright terms: Public domain W3C validator