Step | Hyp | Ref
| Expression |
1 | | imasbas.u |
. . . 4
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
2 | | imasbas.v |
. . . 4
⊢ (𝜑 → 𝑉 = (Base‘𝑅)) |
3 | | eqid 2740 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | eqid 2740 |
. . . 4
⊢
(.r‘𝑅) = (.r‘𝑅) |
5 | | eqid 2740 |
. . . 4
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
6 | | eqid 2740 |
. . . 4
⊢
(Base‘(Scalar‘𝑅)) = (Base‘(Scalar‘𝑅)) |
7 | | eqid 2740 |
. . . 4
⊢ (
·𝑠 ‘𝑅) = ( ·𝑠
‘𝑅) |
8 | | eqid 2740 |
. . . 4
⊢
(·𝑖‘𝑅) =
(·𝑖‘𝑅) |
9 | | imastset.j |
. . . 4
⊢ 𝐽 = (TopOpen‘𝑅) |
10 | | eqid 2740 |
. . . 4
⊢
(dist‘𝑅) =
(dist‘𝑅) |
11 | | eqid 2740 |
. . . 4
⊢
(le‘𝑅) =
(le‘𝑅) |
12 | | imasbas.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
13 | | imasbas.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ 𝑍) |
14 | | eqid 2740 |
. . . . 5
⊢
(+g‘𝑈) = (+g‘𝑈) |
15 | 1, 2, 12, 13, 3, 14 | imasplusg 17226 |
. . . 4
⊢ (𝜑 → (+g‘𝑈) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝(+g‘𝑅)𝑞))〉}) |
16 | | eqid 2740 |
. . . . 5
⊢
(.r‘𝑈) = (.r‘𝑈) |
17 | 1, 2, 12, 13, 4, 16 | imasmulr 17227 |
. . . 4
⊢ (𝜑 → (.r‘𝑈) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝(.r‘𝑅)𝑞))〉}) |
18 | | eqid 2740 |
. . . . 5
⊢ (
·𝑠 ‘𝑈) = ( ·𝑠
‘𝑈) |
19 | 1, 2, 12, 13, 5, 6, 7, 18 | imasvsca 17229 |
. . . 4
⊢ (𝜑 → (
·𝑠 ‘𝑈) = ∪
𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))) |
20 | | eqidd 2741 |
. . . 4
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉} = ∪
𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}) |
21 | | eqidd 2741 |
. . . 4
⊢ (𝜑 → (𝐽 qTop 𝐹) = (𝐽 qTop 𝐹)) |
22 | | eqid 2740 |
. . . . 5
⊢
(dist‘𝑈) =
(dist‘𝑈) |
23 | 1, 2, 12, 13, 10, 22 | imasds 17222 |
. . . 4
⊢ (𝜑 → (dist‘𝑈) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑢 ∈ ℕ ran (𝑧 ∈ {𝑤 ∈ ((𝑉 × 𝑉) ↑m (1...𝑢)) ∣ ((𝐹‘(1st ‘(𝑤‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑤‘𝑢))) = 𝑦 ∧ ∀𝑣 ∈ (1...(𝑢 − 1))(𝐹‘(2nd ‘(𝑤‘𝑣))) = (𝐹‘(1st ‘(𝑤‘(𝑣 + 1)))))} ↦
(ℝ*𝑠 Σg
((dist‘𝑅) ∘
𝑧))), ℝ*,
< ))) |
24 | | eqidd 2741 |
. . . 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 17220 |
. . 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 6775 |
. 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 7304 |
. . 3
⊢ (𝐽 qTop 𝐹) ∈ V |
29 | | eqid 2740 |
. . . . 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 17160 |
. . . 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 17061 |
. . . 4
⊢ TopSet =
Slot (TopSet‘ndx) |
32 | | snsstp1 4755 |
. . . . 5
⊢
{〈(TopSet‘ndx), (𝐽 qTop 𝐹)〉} ⊆ {〈(TopSet‘ndx),
(𝐽 qTop 𝐹)〉, 〈(le‘ndx), ((𝐹 ∘ (le‘𝑅)) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉} |
33 | | ssun2 4112 |
. . . . 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 3935 |
. . . 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 16903 |
. . 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 2805 |
1
⊢ (𝜑 → 𝑂 = (𝐽 qTop 𝐹)) |