| Step | Hyp | Ref
| Expression |
| 1 | | imasbas.u |
. . . 4
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
| 2 | | imasbas.v |
. . . 4
⊢ (𝜑 → 𝑉 = (Base‘𝑅)) |
| 3 | | eqid 2737 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
| 4 | | eqid 2737 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
| 5 | | eqid 2737 |
. . . 4
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
| 6 | | eqid 2737 |
. . . 4
⊢
(Base‘(Scalar‘𝑅)) = (Base‘(Scalar‘𝑅)) |
| 7 | | eqid 2737 |
. . . 4
⊢ (
·𝑠 ‘𝑅) = ( ·𝑠
‘𝑅) |
| 8 | | eqid 2737 |
. . . 4
⊢
(·𝑖‘𝑅) =
(·𝑖‘𝑅) |
| 9 | | imastset.j |
. . . 4
⊢ 𝐽 = (TopOpen‘𝑅) |
| 10 | | eqid 2737 |
. . . 4
⊢
(dist‘𝑅) =
(dist‘𝑅) |
| 11 | | eqid 2737 |
. . . 4
⊢
(le‘𝑅) =
(le‘𝑅) |
| 12 | | imasbas.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
| 13 | | imasbas.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ 𝑍) |
| 14 | | eqid 2737 |
. . . . 5
⊢
(+g‘𝑈) = (+g‘𝑈) |
| 15 | 1, 2, 12, 13, 3, 14 | imasplusg 17562 |
. . . 4
⊢ (𝜑 → (+g‘𝑈) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝(+g‘𝑅)𝑞))〉}) |
| 16 | | eqid 2737 |
. . . . 5
⊢
(.r‘𝑈) = (.r‘𝑈) |
| 17 | 1, 2, 12, 13, 4, 16 | imasmulr 17563 |
. . . 4
⊢ (𝜑 → (.r‘𝑈) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝(.r‘𝑅)𝑞))〉}) |
| 18 | | eqid 2737 |
. . . . 5
⊢ (
·𝑠 ‘𝑈) = ( ·𝑠
‘𝑈) |
| 19 | 1, 2, 12, 13, 5, 6, 7, 18 | imasvsca 17565 |
. . . 4
⊢ (𝜑 → (
·𝑠 ‘𝑈) = ∪
𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))) |
| 20 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉} = ∪
𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}) |
| 21 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → (𝐽 qTop 𝐹) = (𝐽 qTop 𝐹)) |
| 22 | | eqid 2737 |
. . . . 5
⊢
(dist‘𝑈) =
(dist‘𝑈) |
| 23 | 1, 2, 12, 13, 10, 22 | imasds 17558 |
. . . 4
⊢ (𝜑 → (dist‘𝑈) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑢 ∈ ℕ ran (𝑧 ∈ {𝑤 ∈ ((𝑉 × 𝑉) ↑m (1...𝑢)) ∣ ((𝐹‘(1st ‘(𝑤‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑤‘𝑢))) = 𝑦 ∧ ∀𝑣 ∈ (1...(𝑢 − 1))(𝐹‘(2nd ‘(𝑤‘𝑣))) = (𝐹‘(1st ‘(𝑤‘(𝑣 + 1)))))} ↦
(ℝ*𝑠 Σg
((dist‘𝑅) ∘
𝑧))), ℝ*,
< ))) |
| 24 | | eqidd 2738 |
. . . 4
⊢ (𝜑 → ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹) = ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)) |
| 25 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 15, 17, 19, 20, 21, 23, 24, 12, 13 | imasval 17556 |
. . 3
⊢ (𝜑 → 𝑈 = (({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (𝐽
qTop 𝐹)〉,
〈(le‘ndx), ((𝐹
∘ (le‘𝑅)) ∘
◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉})) |
| 26 | 25 | fveq2d 6910 |
. 2
⊢ (𝜑 → (TopSet‘𝑈) =
(TopSet‘(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (𝐽
qTop 𝐹)〉,
〈(le‘ndx), ((𝐹
∘ (le‘𝑅)) ∘
◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}))) |
| 27 | | imastset.o |
. 2
⊢ 𝑂 = (TopSet‘𝑈) |
| 28 | | ovex 7464 |
. . 3
⊢ (𝐽 qTop 𝐹) ∈ V |
| 29 | | eqid 2737 |
. . . . 5
⊢
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (𝐽
qTop 𝐹)〉,
〈(le‘ndx), ((𝐹
∘ (le‘𝑅)) ∘
◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) =
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉,
〈(.r‘ndx), (.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝
∈ 𝑉 ∪ 𝑞
∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (𝐽
qTop 𝐹)〉,
〈(le‘ndx), ((𝐹
∘ (le‘𝑅)) ∘
◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) |
| 30 | 29 | imasvalstr 17496 |
. . . 4
⊢
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (𝐽
qTop 𝐹)〉,
〈(le‘ndx), ((𝐹
∘ (le‘𝑅)) ∘
◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) Struct
〈1, ;12〉 |
| 31 | | tsetid 17397 |
. . . 4
⊢ TopSet =
Slot (TopSet‘ndx) |
| 32 | | snsstp1 4816 |
. . . . 5
⊢
{〈(TopSet‘ndx), (𝐽 qTop 𝐹)〉} ⊆ {〈(TopSet‘ndx),
(𝐽 qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉} |
| 33 | | ssun2 4179 |
. . . . 5
⊢
{〈(TopSet‘ndx), (𝐽 qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}
⊆ (({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (𝐽
qTop 𝐹)〉,
〈(le‘ndx), ((𝐹
∘ (le‘𝑅)) ∘
◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) |
| 34 | 32, 33 | sstri 3993 |
. . . 4
⊢
{〈(TopSet‘ndx), (𝐽 qTop 𝐹)〉} ⊆ (({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (𝐽
qTop 𝐹)〉,
〈(le‘ndx), ((𝐹
∘ (le‘𝑅)) ∘
◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) |
| 35 | 30, 31, 34 | strfv 17240 |
. . 3
⊢ ((𝐽 qTop 𝐹) ∈ V → (𝐽 qTop 𝐹) = (TopSet‘(({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (𝐽
qTop 𝐹)〉,
〈(le‘ndx), ((𝐹
∘ (le‘𝑅)) ∘
◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}))) |
| 36 | 28, 35 | ax-mp 5 |
. 2
⊢ (𝐽 qTop 𝐹) = (TopSet‘(({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (𝐽
qTop 𝐹)〉,
〈(le‘ndx), ((𝐹
∘ (le‘𝑅)) ∘
◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉})) |
| 37 | 26, 27, 36 | 3eqtr4g 2802 |
1
⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹)) |