| Step | Hyp | Ref
| Expression |
| 1 | | rlocval.19 |
. . 3
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
| 2 | 1 | elexd 3504 |
. 2
⊢ (𝜑 → 𝑅 ∈ V) |
| 3 | | rlocval.1 |
. . . . 5
⊢ 𝐵 = (Base‘𝑅) |
| 4 | 3 | fvexi 6920 |
. . . 4
⊢ 𝐵 ∈ V |
| 5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐵 ∈ V) |
| 6 | | rlocval.20 |
. . 3
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
| 7 | 5, 6 | ssexd 5324 |
. 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 6921 |
. . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (.r‘𝑟) ∈ V) |
| 10 | | fveq2 6906 |
. . . . . 6
⊢ (𝑟 = 𝑅 → (.r‘𝑟) = (.r‘𝑅)) |
| 11 | 10 | adantr 480 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (.r‘𝑟) = (.r‘𝑅)) |
| 12 | | rlocval.3 |
. . . . 5
⊢ · =
(.r‘𝑅) |
| 13 | 11, 12 | eqtr4di 2795 |
. . . 4
⊢ ((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) → (.r‘𝑟) = · ) |
| 14 | | fvexd 6921 |
. . . . . 6
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
(Base‘𝑟) ∈
V) |
| 15 | | vex 3484 |
. . . . . . 7
⊢ 𝑠 ∈ V |
| 16 | 15 | a1i 11 |
. . . . . 6
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → 𝑠 ∈ V) |
| 17 | 14, 16 | xpexd 7771 |
. . . . 5
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
((Base‘𝑟) ×
𝑠) ∈
V) |
| 18 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
| 19 | 18 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
(Base‘𝑟) =
(Base‘𝑅)) |
| 20 | 19, 3 | eqtr4di 2795 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
(Base‘𝑟) = 𝐵) |
| 21 | | simplr 769 |
. . . . . . 7
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) → 𝑠 = 𝑆) |
| 22 | 20, 21 | xpeq12d 5716 |
. . . . . 6
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
((Base‘𝑟) ×
𝑠) = (𝐵 × 𝑆)) |
| 23 | | rlocval.10 |
. . . . . 6
⊢ 𝑊 = (𝐵 × 𝑆) |
| 24 | 22, 23 | eqtr4di 2795 |
. . . . 5
⊢ (((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) →
((Base‘𝑟) ×
𝑠) = 𝑊) |
| 25 | | simpr 484 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑤 = 𝑊) |
| 26 | 25 | opeq2d 4880 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 〈(Base‘ndx), 𝑤〉 = 〈(Base‘ndx),
𝑊〉) |
| 27 | | simplll 775 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑟 = 𝑅) |
| 28 | 27 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (+g‘𝑟) = (+g‘𝑅)) |
| 29 | | rlocval.5 |
. . . . . . . . . . . . . . 15
⊢ + =
(+g‘𝑅) |
| 30 | 28, 29 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (+g‘𝑟) = + ) |
| 31 | | simplr 769 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑥 = · ) |
| 32 | 31 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st ‘𝑎)𝑥(2nd ‘𝑏)) = ((1st ‘𝑎) · (2nd
‘𝑏))) |
| 33 | 31 | oveqd 7448 |
. . . . . . . . . . . . . 14
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st ‘𝑏)𝑥(2nd ‘𝑎)) = ((1st ‘𝑏) · (2nd
‘𝑎))) |
| 34 | 30, 32, 33 | oveq123d 7452 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))) = (((1st ‘𝑎) · (2nd
‘𝑏)) +
((1st ‘𝑏)
·
(2nd ‘𝑎)))) |
| 35 | 31 | oveqd 7448 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((2nd ‘𝑎)𝑥(2nd ‘𝑏)) = ((2nd ‘𝑎) · (2nd
‘𝑏))) |
| 36 | 34, 35 | opeq12d 4881 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 〈(((1st
‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))〉 = 〈(((1st
‘𝑎) ·
(2nd ‘𝑏))
+
((1st ‘𝑏)
·
(2nd ‘𝑎))), ((2nd ‘𝑎) · (2nd
‘𝑏))〉) |
| 37 | 25, 25, 36 | mpoeq123dv 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
‘𝑏))〉) |
| 39 | 37, 38 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ 〈(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))〉) = ⊕ ) |
| 40 | 39 | opeq2d 4880 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 〈(+g‘ndx),
(𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ 〈(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))〉)〉 =
〈(+g‘ndx), ⊕
〉) |
| 41 | 31 | oveqd 7448 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((1st ‘𝑎)𝑥(1st ‘𝑏)) = ((1st ‘𝑎) · (1st
‘𝑏))) |
| 42 | 41, 35 | opeq12d 4881 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 〈((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))〉 = 〈((1st
‘𝑎) ·
(1st ‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉) |
| 43 | 25, 25, 42 | mpoeq123dv 7508 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ 〈((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))〉) = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈((1st ‘𝑎) · (1st
‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)) |
| 44 | | rlocval.15 |
. . . . . . . . . . 11
⊢ ⊗ =
(𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈((1st ‘𝑎) · (1st
‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉) |
| 45 | 43, 44 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ 〈((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))〉) = ⊗ ) |
| 46 | 45 | opeq2d 4880 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 〈(.r‘ndx),
(𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ 〈((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))〉)〉 =
〈(.r‘ndx), ⊗
〉) |
| 47 | 26, 40, 46 | tpeq123d 4748 |
. . . . . . . 8
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {〈(Base‘ndx), 𝑤〉,
〈(+g‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ 〈(((1st ‘𝑎)𝑥(2nd ‘𝑏))(+g‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))〉)〉,
〈(.r‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ 〈((1st ‘𝑎)𝑥(1st ‘𝑏)), ((2nd ‘𝑎)𝑥(2nd ‘𝑏))〉)〉} = {〈(Base‘ndx),
𝑊〉,
〈(+g‘ndx), ⊕ 〉,
〈(.r‘ndx), ⊗
〉}) |
| 48 | 27 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Scalar‘𝑟) = (Scalar‘𝑅)) |
| 49 | | rlocval.7 |
. . . . . . . . . . 11
⊢ 𝐹 = (Scalar‘𝑅) |
| 50 | 48, 49 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Scalar‘𝑟) = 𝐹) |
| 51 | 50 | opeq2d 4880 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 〈(Scalar‘ndx),
(Scalar‘𝑟)〉 =
〈(Scalar‘ndx), 𝐹〉) |
| 52 | 48 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Base‘(Scalar‘𝑟)) =
(Base‘(Scalar‘𝑅))) |
| 53 | | rlocval.8 |
. . . . . . . . . . . . . 14
⊢ 𝐾 = (Base‘𝐹) |
| 54 | 49 | fveq2i 6909 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝐹) =
(Base‘(Scalar‘𝑅)) |
| 55 | 53, 54 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ 𝐾 =
(Base‘(Scalar‘𝑅)) |
| 56 | 52, 55 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (Base‘(Scalar‘𝑟)) = 𝐾) |
| 57 | 27 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (
·𝑠 ‘𝑟) = ( ·𝑠
‘𝑅)) |
| 58 | | rlocval.9 |
. . . . . . . . . . . . . . 15
⊢ 𝐶 = (
·𝑠 ‘𝑅) |
| 59 | 57, 58 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (
·𝑠 ‘𝑟) = 𝐶) |
| 60 | 59 | oveqd 7448 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑘( ·𝑠
‘𝑟)(1st
‘𝑎)) = (𝑘𝐶(1st ‘𝑎))) |
| 61 | 60 | opeq1d 4879 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 〈(𝑘( ·𝑠
‘𝑟)(1st
‘𝑎)), (2nd
‘𝑎)〉 =
〈(𝑘𝐶(1st ‘𝑎)), (2nd ‘𝑎)〉) |
| 62 | 56, 25, 61 | mpoeq123dv 7508 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ 〈(𝑘( ·𝑠
‘𝑟)(1st
‘𝑎)), (2nd
‘𝑎)〉) = (𝑘 ∈ 𝐾, 𝑎 ∈ 𝑊 ↦ 〈(𝑘𝐶(1st ‘𝑎)), (2nd ‘𝑎)〉)) |
| 63 | | rlocval.16 |
. . . . . . . . . . 11
⊢ × =
(𝑘 ∈ 𝐾, 𝑎 ∈ 𝑊 ↦ 〈(𝑘𝐶(1st ‘𝑎)), (2nd ‘𝑎)〉) |
| 64 | 62, 63 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ 〈(𝑘( ·𝑠
‘𝑟)(1st
‘𝑎)), (2nd
‘𝑎)〉) = ×
) |
| 65 | 64 | opeq2d 4880 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 〈(
·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ 〈(𝑘( ·𝑠
‘𝑟)(1st
‘𝑎)), (2nd
‘𝑎)〉)〉 =
〈( ·𝑠 ‘ndx), ×
〉) |
| 66 | | eqidd 2738 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) →
〈(·𝑖‘ndx), ∅〉 =
〈(·𝑖‘ndx),
∅〉) |
| 67 | 51, 65, 66 | tpeq123d 4748 |
. . . . . . . 8
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {〈(Scalar‘ndx),
(Scalar‘𝑟)〉,
〈( ·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑟)), 𝑎 ∈ 𝑤 ↦ 〈(𝑘( ·𝑠
‘𝑟)(1st
‘𝑎)), (2nd
‘𝑎)〉)〉,
〈(·𝑖‘ndx), ∅〉} =
{〈(Scalar‘ndx), 𝐹〉, 〈(
·𝑠 ‘ndx), × 〉,
〈(·𝑖‘ndx),
∅〉}) |
| 68 | 47, 67 | uneq12d 4169 |
. . . . . . 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),
∅〉})) |
| 69 | 27 | fveq2d 6910 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (TopSet‘𝑟) = (TopSet‘𝑅)) |
| 70 | | rlocval.12 |
. . . . . . . . . . 11
⊢ 𝐽 = (TopSet‘𝑅) |
| 71 | 69, 70 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (TopSet‘𝑟) = 𝐽) |
| 72 | 21 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 𝑠 = 𝑆) |
| 73 | 71, 72 | oveq12d 7449 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((TopSet‘𝑟) ↾t 𝑠) = (𝐽 ↾t 𝑆)) |
| 74 | 71, 73 | oveq12d 7449 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((TopSet‘𝑟) ×t ((TopSet‘𝑟) ↾t 𝑠)) = (𝐽 ×t (𝐽 ↾t 𝑆))) |
| 75 | 74 | opeq2d 4880 |
. . . . . . . 8
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 〈(TopSet‘ndx),
((TopSet‘𝑟)
×t ((TopSet‘𝑟) ↾t 𝑠))〉 = 〈(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))〉) |
| 76 | 25 | eleq2d 2827 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤 ↔ 𝑎 ∈ 𝑊)) |
| 77 | 25 | eleq2d 2827 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑏 ∈ 𝑤 ↔ 𝑏 ∈ 𝑊)) |
| 78 | 76, 77 | anbi12d 632 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ↔ (𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊))) |
| 79 | 27 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (le‘𝑟) = (le‘𝑅)) |
| 80 | | rlocval.6 |
. . . . . . . . . . . . . 14
⊢ ≤ =
(le‘𝑅) |
| 81 | 79, 80 | eqtr4di 2795 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (le‘𝑟) = ≤ ) |
| 82 | 32, 81, 33 | breq123d 5157 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)) ↔ ((1st ‘𝑎) · (2nd
‘𝑏)) ≤
((1st ‘𝑏)
·
(2nd ‘𝑎)))) |
| 83 | 78, 82 | anbi12d 632 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))) ↔ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd
‘𝑏)) ≤
((1st ‘𝑏)
·
(2nd ‘𝑎))))) |
| 84 | 83 | opabbidv 5209 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd
‘𝑏)) ≤
((1st ‘𝑏)
·
(2nd ‘𝑎)))}) |
| 85 | | rlocval.17 |
. . . . . . . . . 10
⊢ ≲ =
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd
‘𝑏)) ≤
((1st ‘𝑏)
·
(2nd ‘𝑎)))} |
| 86 | 84, 85 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))} = ≲ ) |
| 87 | 86 | opeq2d 4880 |
. . . . . . . 8
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 〈(le‘ndx), {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑤 ∧ 𝑏 ∈ 𝑤) ∧ ((1st ‘𝑎)𝑥(2nd ‘𝑏))(le‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))}〉 = 〈(le‘ndx), ≲
〉) |
| 88 | 27 | fveq2d 6910 |
. . . . . . . . . . . . 13
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (dist‘𝑟) = (dist‘𝑅)) |
| 89 | | rlocval.13 |
. . . . . . . . . . . . 13
⊢ 𝐷 = (dist‘𝑅) |
| 90 | 88, 89 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (dist‘𝑟) = 𝐷) |
| 91 | 90, 32, 33 | oveq123d 7452 |
. . . . . . . . . . 11
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))) = (((1st ‘𝑎) · (2nd
‘𝑏))𝐷((1st ‘𝑏) · (2nd
‘𝑎)))) |
| 92 | 25, 25, 91 | mpoeq123dv 7508 |
. . . . . . . . . 10
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ (((1st ‘𝑎) · (2nd
‘𝑏))𝐷((1st ‘𝑏) · (2nd
‘𝑎))))) |
| 93 | | rlocval.18 |
. . . . . . . . . 10
⊢ 𝐸 = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ (((1st ‘𝑎) · (2nd
‘𝑏))𝐷((1st ‘𝑏) · (2nd
‘𝑎)))) |
| 94 | 92, 93 | eqtr4di 2795 |
. . . . . . . . 9
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎)))) = 𝐸) |
| 95 | 94 | opeq2d 4880 |
. . . . . . . 8
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → 〈(dist‘ndx), (𝑎 ∈ 𝑤, 𝑏 ∈ 𝑤 ↦ (((1st ‘𝑎)𝑥(2nd ‘𝑏))(dist‘𝑟)((1st ‘𝑏)𝑥(2nd ‘𝑎))))〉 = 〈(dist‘ndx), 𝐸〉) |
| 96 | 75, 87, 95 | tpeq123d 4748 |
. . . . . . 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), 𝐸〉}) |
| 97 | 68, 96 | uneq12d 4169 |
. . . . . 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), 𝐸〉})) |
| 98 | 27, 72 | oveq12d 7449 |
. . . . . . 7
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑟 ~RL 𝑠) = (𝑅 ~RL 𝑆)) |
| 99 | | rlocval.11 |
. . . . . . 7
⊢ ∼ =
(𝑅 ~RL
𝑆) |
| 100 | 98, 99 | eqtr4di 2795 |
. . . . . 6
⊢ ((((𝑟 = 𝑅 ∧ 𝑠 = 𝑆) ∧ 𝑥 = · ) ∧ 𝑤 = 𝑊) → (𝑟 ~RL 𝑠) = ∼ ) |
| 101 | 97, 100 | oveq12d 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 ∼
)) |
| 102 | 17, 24, 101 | csbied2 3936 |
. . . 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 ∼
)) |
| 103 | 9, 13, 102 | csbied2 3936 |
. . 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 33260 |
. . 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 𝑠))) |
| 105 | 103, 104 | ovmpoga 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 ∼
)) |
| 106 | 2, 7, 8, 105 | syl3anc 1373 |
1
⊢ (𝜑 → (𝑅 RLocal 𝑆) = ((({〈(Base‘ndx), 𝑊〉,
〈(+g‘ndx), ⊕ 〉,
〈(.r‘ndx), ⊗ 〉} ∪
{〈(Scalar‘ndx), 𝐹〉, 〈(
·𝑠 ‘ndx), × 〉,
〈(·𝑖‘ndx), ∅〉}) ∪
{〈(TopSet‘ndx), (𝐽 ×t (𝐽 ↾t 𝑆))〉, 〈(le‘ndx), ≲
〉, 〈(dist‘ndx), 𝐸〉}) /s ∼
)) |