| 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 2737 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 7 | | eqid 2737 |
. . . 4
⊢
(le‘𝑅) =
(le‘𝑅) |
| 8 | | eqid 2737 |
. . . 4
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
| 9 | | eqid 2737 |
. . . 4
⊢
(Base‘(Scalar‘𝑅)) = (Base‘(Scalar‘𝑅)) |
| 10 | | eqid 2737 |
. . . 4
⊢ (
·𝑠 ‘𝑅) = ( ·𝑠
‘𝑅) |
| 11 | | rlocbas.w |
. . . 4
⊢ 𝑊 = (𝐵 × 𝑆) |
| 12 | | rlocbas.4 |
. . . 4
⊢ ∼ =
(𝑅 ~RL
𝑆) |
| 13 | | eqid 2737 |
. . . 4
⊢
(TopSet‘𝑅) =
(TopSet‘𝑅) |
| 14 | | eqid 2737 |
. . . 4
⊢
(dist‘𝑅) =
(dist‘𝑅) |
| 15 | | eqid 2737 |
. . . 4
⊢ (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈(((1st
‘𝑎) ·
(2nd ‘𝑏))(+g‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎))),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉) = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈(((1st
‘𝑎) ·
(2nd ‘𝑏))(+g‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎))),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉) |
| 16 | | eqid 2737 |
. . . 4
⊢ (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈((1st ‘𝑎) · (1st
‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉) = (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈((1st ‘𝑎) · (1st
‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉) |
| 17 | | eqid 2737 |
. . . 4
⊢ (𝑘 ∈
(Base‘(Scalar‘𝑅)), 𝑎 ∈ 𝑊 ↦ 〈(𝑘( ·𝑠
‘𝑅)(1st
‘𝑎)), (2nd
‘𝑎)〉) = (𝑘 ∈
(Base‘(Scalar‘𝑅)), 𝑎 ∈ 𝑊 ↦ 〈(𝑘( ·𝑠
‘𝑅)(1st
‘𝑎)), (2nd
‘𝑎)〉) |
| 18 | | eqid 2737 |
. . . 4
⊢
{〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd
‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎)))} = {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ 𝑊 ∧ 𝑏 ∈ 𝑊) ∧ ((1st ‘𝑎) · (2nd
‘𝑏))(le‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎)))} |
| 19 | | eqid 2737 |
. . . 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 33263 |
. . 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 2789 |
. 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 2738 |
. . . 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 2737 |
. . . . 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 17496 |
. . . 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 17250 |
. . . 4
⊢ Base =
Slot (Base‘ndx) |
| 28 | | snsstp1 4816 |
. . . . 5
⊢
{〈(Base‘ndx), 𝑊〉} ⊆ {〈(Base‘ndx),
𝑊〉,
〈(+g‘ndx), (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈(((1st
‘𝑎) ·
(2nd ‘𝑏))(+g‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎))),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)〉,
〈(.r‘ndx), (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈((1st ‘𝑎) · (1st
‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)〉} |
| 29 | | ssun1 4178 |
. . . . . 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 4178 |
. . . . . 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 3993 |
. . . . 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 3993 |
. . . 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 6920 |
. . . . . . 7
⊢ 𝐵 ∈ V |
| 34 | 33 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ V) |
| 35 | 34, 21 | ssexd 5324 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ V) |
| 36 | 34, 35 | xpexd 7771 |
. . . . 5
⊢ (𝜑 → (𝐵 × 𝑆) ∈ V) |
| 37 | 11, 36 | eqeltrid 2845 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ V) |
| 38 | | eqid 2737 |
. . . 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 17241 |
. . 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 2743 |
. 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 7465 |
. . 3
⊢ ∼ ∈
V |
| 42 | 41 | a1i 11 |
. 2
⊢ (𝜑 → ∼ ∈
V) |
| 43 | | tpex 7766 |
. . . . 5
⊢
{〈(Base‘ndx), 𝑊〉, 〈(+g‘ndx),
(𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈(((1st
‘𝑎) ·
(2nd ‘𝑏))(+g‘𝑅)((1st ‘𝑏) · (2nd
‘𝑎))),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)〉,
〈(.r‘ndx), (𝑎 ∈ 𝑊, 𝑏 ∈ 𝑊 ↦ 〈((1st ‘𝑎) · (1st
‘𝑏)),
((2nd ‘𝑎)
·
(2nd ‘𝑏))〉)〉} ∈ V |
| 44 | | tpex 7766 |
. . . . 5
⊢
{〈(Scalar‘ndx), (Scalar‘𝑅)〉, 〈(
·𝑠 ‘ndx), (𝑘 ∈ (Base‘(Scalar‘𝑅)), 𝑎 ∈ 𝑊 ↦ 〈(𝑘( ·𝑠
‘𝑅)(1st
‘𝑎)), (2nd
‘𝑎)〉)〉,
〈(·𝑖‘ndx), ∅〉} ∈
V |
| 45 | 43, 44 | unex 7764 |
. . . 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 7766 |
. . . 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 7764 |
. . 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 17590 |
1
⊢ (𝜑 → (𝑊 / ∼ ) =
(Base‘𝐿)) |