Step | Hyp | Ref
| Expression |
1 | | rlocbas.l |
. . 3
⊢ 𝐿 = (𝑅 RLocal 𝑆) |
2 | | rlocbas.b |
. . . 4
⊢ 𝐵 = (Base‘𝑅) |
3 | | rlocbas.1 |
. . . 4
⊢ 0 =
(0g‘𝑅) |
4 | | rlocbas.2 |
. . . 4
⊢ · =
(.r‘𝑅) |
5 | | rlocbas.3 |
. . . 4
⊢ − =
(-g‘𝑅) |
6 | | eqid 2740 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
7 | | eqid 2740 |
. . . 4
⊢
(le‘𝑅) =
(le‘𝑅) |
8 | | eqid 2740 |
. . . 4
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
9 | | eqid 2740 |
. . . 4
⊢
(Base‘(Scalar‘𝑅)) = (Base‘(Scalar‘𝑅)) |
10 | | eqid 2740 |
. . . 4
⊢ (
·𝑠 ‘𝑅) = ( ·𝑠
‘𝑅) |
11 | | rlocbas.w |
. . . 4
⊢ 𝑊 = (𝐵 × 𝑆) |
12 | | rlocbas.4 |
. . . 4
⊢ ∼ =
(𝑅 ~RL
𝑆) |
13 | | eqid 2740 |
. . . 4
⊢
(TopSet‘𝑅) =
(TopSet‘𝑅) |
14 | | eqid 2740 |
. . . 4
⊢
(dist‘𝑅) =
(dist‘𝑅) |
15 | | eqid 2740 |
. . . 4
⊢ (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈(((1st
‘𝑎) ·
(2nd ‘𝑏))(+g‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎))),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉) = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈(((1st
‘𝑎) ·
(2nd ‘𝑏))(+g‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎))),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉) |
16 | | eqid 2740 |
. . . 4
⊢ (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈((1st ‘𝑎) · (1st
‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉) = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈((1st ‘𝑎) · (1st
‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉) |
17 | | eqid 2740 |
. . . 4
⊢ (𝑘 ∈
(Base‘(Scalar‘𝑅)), 𝑎 ∈ 𝑊 ↦ 〈(𝑘( ·𝑠
‘𝑅)(1st
‘𝑎)), (2nd
‘𝑎)〉) = (𝑘 ∈
(Base‘(Scalar‘𝑅)), 𝑎 ∈ 𝑊 ↦ 〈(𝑘( ·𝑠
‘𝑅)(1st
‘𝑎)), (2nd
‘𝑎)〉) |
18 | | eqid 2740 |
. . . 4
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd
‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎)))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd
‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎)))} |
19 | | eqid 2740 |
. . . 4
⊢ (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ (((1st ‘𝑎) · (2nd
‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎)))) = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ (((1st ‘𝑎) · (2nd
‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎)))) |
20 | | rlocbas.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑉) |
21 | | rlocbas.s |
. . . 4
⊢ (𝜑 → 𝑆 ⊆ 𝐵) |
22 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 | rlocval 33231 |
. . 3
⊢ (𝜑 → (𝑅 RLocal 𝑆) = ((({〈(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 ∼ )) |
23 | 1, 22 | eqtrid 2792 |
. 2
⊢ (𝜑 → 𝐿 = ((({〈(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 ∼ )) |
24 | | eqidd 2741 |
. . . 4
⊢ (𝜑 → (({〈(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),
(𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈(((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
‘𝑎))))〉})) |
25 | | eqid 2740 |
. . . . 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
‘𝑎))))〉}) =
(({〈(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
‘𝑎))))〉}) |
26 | 25 | imasvalstr 17511 |
. . . 4
⊢
(({〈(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
‘𝑎))))〉}) Struct
〈1, ;12〉 |
27 | | baseid 17261 |
. . . 4
⊢ Base =
Slot (Base‘ndx) |
28 | | snsstp1 4841 |
. . . . 5
⊢
{〈(Base‘ndx), 𝑊〉} ⊆ {〈(Base‘ndx),
𝑊〉,
〈(+g‘ndx), (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈(((1st
‘𝑎) ·
(2nd ‘𝑏))(+g‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎))),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)〉,
〈(.r‘ndx), (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈((1st ‘𝑎) · (1st
‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)〉} |
29 | | ssun1 4201 |
. . . . . 6
⊢
{〈(Base‘ndx), 𝑊〉, 〈(+g‘ndx),
(𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈(((1st
‘𝑎) ·
(2nd ‘𝑏))(+g‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎))),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)〉,
〈(.r‘ndx), (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈((1st ‘𝑎) · (1st
‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)〉} ⊆
({〈(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),
∅〉}) |
30 | | ssun1 4201 |
. . . . . 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), ∅〉}) ⊆
(({〈(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
‘𝑎))))〉}) |
31 | 29, 30 | sstri 4018 |
. . . . 5
⊢
{〈(Base‘ndx), 𝑊〉, 〈(+g‘ndx),
(𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈(((1st
‘𝑎) ·
(2nd ‘𝑏))(+g‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎))),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)〉,
〈(.r‘ndx), (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈((1st ‘𝑎) · (1st
‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)〉} ⊆
(({〈(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
‘𝑎))))〉}) |
32 | 28, 31 | sstri 4018 |
. . . 4
⊢
{〈(Base‘ndx), 𝑊〉} ⊆ (({〈(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
‘𝑎))))〉}) |
33 | 2 | fvexi 6934 |
. . . . . . 7
⊢ 𝐵 ∈ V |
34 | 33 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ V) |
35 | 34, 21 | ssexd 5342 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ V) |
36 | 34, 35 | xpexd 7786 |
. . . . 5
⊢ (𝜑 → (𝐵 × 𝑆) ∈ V) |
37 | 11, 36 | eqeltrid 2848 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ V) |
38 | | eqid 2740 |
. . . 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
‘𝑎))))〉})) =
(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
‘𝑎))))〉})) |
39 | 24, 26, 27, 32, 37, 38 | strfv3 17252 |
. . 3
⊢ (𝜑 →
(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
‘𝑎))))〉})) =
𝑊) |
40 | 39 | eqcomd 2746 |
. 2
⊢ (𝜑 → 𝑊 = (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
‘𝑎))))〉}))) |
41 | 12 | ovexi 7482 |
. . 3
⊢ ∼ ∈
V |
42 | 41 | a1i 11 |
. 2
⊢ (𝜑 → ∼ ∈
V) |
43 | | tpex 7781 |
. . . . 5
⊢
{〈(Base‘ndx), 𝑊〉, 〈(+g‘ndx),
(𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈(((1st
‘𝑎) ·
(2nd ‘𝑏))(+g‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎))),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)〉,
〈(.r‘ndx), (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈((1st ‘𝑎) · (1st
‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)〉} ∈ V |
44 | | tpex 7781 |
. . . . 5
⊢
{〈(Scalar‘ndx), (Scalar‘𝑅)〉, 〈(
·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ 𝑊 ↦ 〈(𝑘( ·𝑠
‘𝑅)(1st
‘𝑎)), (2nd
‘𝑎)〉)〉,
〈(·𝑖‘ndx), ∅〉} ∈
V |
45 | 43, 44 | unex 7779 |
. . . 4
⊢
({〈(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), ∅〉}) ∈
V |
46 | | tpex 7781 |
. . . 4
⊢
{〈(TopSet‘ndx), ((TopSet‘𝑅) ×t ((TopSet‘𝑅) ↾t 𝑆))〉, 〈(le‘ndx),
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd
‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎)))}〉,
〈(dist‘ndx), (𝑎
∈ 𝑊, 𝑏 ∈ 𝑊 ↦ (((1st ‘𝑎) · (2nd
‘𝑏))(dist‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎))))〉} ∈
V |
47 | 45, 46 | unex 7779 |
. . 3
⊢
(({〈(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
‘𝑎))))〉}) ∈
V |
48 | 47 | a1i 11 |
. 2
⊢ (𝜑 → (({〈(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
‘𝑎))))〉}) ∈
V) |
49 | 23, 40, 42, 48 | qusbas 17605 |
1
⊢ (𝜑 → (𝑊 / ∼ ) =
(Base‘𝐿)) |