1 |
|
df-rloc |
⊢ 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 𝑠 ) ) ) |