Step | Hyp | Ref
| Expression |
1 | | imasbas.u |
. . 3
⊢ (𝜑 → 𝑈 = (𝐹 “s 𝑅)) |
2 | | imasbas.v |
. . 3
⊢ (𝜑 → 𝑉 = (Base‘𝑅)) |
3 | | eqid 2610 |
. . 3
⊢
(+g‘𝑅) = (+g‘𝑅) |
4 | | eqid 2610 |
. . 3
⊢
(.r‘𝑅) = (.r‘𝑅) |
5 | | eqid 2610 |
. . 3
⊢
(Scalar‘𝑅) =
(Scalar‘𝑅) |
6 | | eqid 2610 |
. . 3
⊢
(Base‘(Scalar‘𝑅)) = (Base‘(Scalar‘𝑅)) |
7 | | eqid 2610 |
. . 3
⊢ (
·𝑠 ‘𝑅) = ( ·𝑠
‘𝑅) |
8 | | eqid 2610 |
. . 3
⊢
(·𝑖‘𝑅) =
(·𝑖‘𝑅) |
9 | | eqid 2610 |
. . 3
⊢
(TopOpen‘𝑅) =
(TopOpen‘𝑅) |
10 | | eqid 2610 |
. . 3
⊢
(dist‘𝑅) =
(dist‘𝑅) |
11 | | imasle.n |
. . 3
⊢ 𝑁 = (le‘𝑅) |
12 | | imasbas.f |
. . . 4
⊢ (𝜑 → 𝐹:𝑉–onto→𝐵) |
13 | | imasbas.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑍) |
14 | | eqid 2610 |
. . . 4
⊢
(+g‘𝑈) = (+g‘𝑈) |
15 | 1, 2, 12, 13, 3, 14 | imasplusg 16000 |
. . 3
⊢ (𝜑 → (+g‘𝑈) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝(+g‘𝑅)𝑞))〉}) |
16 | | eqid 2610 |
. . . 4
⊢
(.r‘𝑈) = (.r‘𝑈) |
17 | 1, 2, 12, 13, 4, 16 | imasmulr 16001 |
. . 3
⊢ (𝜑 → (.r‘𝑈) = ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝐹‘(𝑝(.r‘𝑅)𝑞))〉}) |
18 | | eqid 2610 |
. . . 4
⊢ (
·𝑠 ‘𝑈) = ( ·𝑠
‘𝑈) |
19 | 1, 2, 12, 13, 5, 6, 7, 18 | imasvsca 16003 |
. . 3
⊢ (𝜑 → (
·𝑠 ‘𝑈) = ∪
𝑞 ∈ 𝑉 (𝑝 ∈ (Base‘(Scalar‘𝑅)), 𝑥 ∈ {(𝐹‘𝑞)} ↦ (𝐹‘(𝑝( ·𝑠
‘𝑅)𝑞)))) |
20 | | eqidd 2611 |
. . 3
⊢ (𝜑 → ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉} = ∪
𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}) |
21 | | eqid 2610 |
. . . 4
⊢
(TopSet‘𝑈) =
(TopSet‘𝑈) |
22 | 1, 2, 12, 13, 9, 21 | imastset 16005 |
. . 3
⊢ (𝜑 → (TopSet‘𝑈) = ((TopOpen‘𝑅) qTop 𝐹)) |
23 | | eqid 2610 |
. . . 4
⊢
(dist‘𝑈) =
(dist‘𝑈) |
24 | 1, 2, 12, 13, 10, 23 | imasds 15996 |
. . 3
⊢ (𝜑 → (dist‘𝑈) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ inf(∪ 𝑢 ∈ ℕ ran (𝑧 ∈ {𝑤 ∈ ((𝑉 × 𝑉) ↑𝑚 (1...𝑢)) ∣ ((𝐹‘(1st ‘(𝑤‘1))) = 𝑥 ∧ (𝐹‘(2nd ‘(𝑤‘𝑢))) = 𝑦 ∧ ∀𝑣 ∈ (1...(𝑢 − 1))(𝐹‘(2nd ‘(𝑤‘𝑣))) = (𝐹‘(1st ‘(𝑤‘(𝑣 + 1)))))} ↦
(ℝ*𝑠 Σg
((dist‘𝑅) ∘
𝑧))), ℝ*,
< ))) |
25 | | eqidd 2611 |
. . 3
⊢ (𝜑 → ((𝐹 ∘ 𝑁) ∘ ◡𝐹) = ((𝐹 ∘ 𝑁) ∘ ◡𝐹)) |
26 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 15, 17, 19, 20, 22, 24, 25, 12, 13 | imasval 15994 |
. 2
⊢ (𝜑 → 𝑈 = (({〈(Base‘ndx), 𝐵〉,
〈(+g‘ndx), (+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (TopSet‘𝑈)〉, 〈(le‘ndx), ((𝐹 ∘ 𝑁) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉})) |
27 | | eqid 2610 |
. . 3
⊢
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (TopSet‘𝑈)〉, 〈(le‘ndx), ((𝐹 ∘ 𝑁) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) =
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉,
〈(.r‘ndx), (.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝
∈ 𝑉 ∪ 𝑞
∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (TopSet‘𝑈)〉, 〈(le‘ndx), ((𝐹 ∘ 𝑁) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) |
28 | 27 | imasvalstr 15935 |
. 2
⊢
(({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (TopSet‘𝑈)〉, 〈(le‘ndx), ((𝐹 ∘ 𝑁) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) Struct
〈1, ;12〉 |
29 | | pleid 15872 |
. 2
⊢ le = Slot
(le‘ndx) |
30 | | snsstp2 4288 |
. . 3
⊢
{〈(le‘ndx), ((𝐹 ∘ 𝑁) ∘ ◡𝐹)〉} ⊆ {〈(TopSet‘ndx),
(TopSet‘𝑈)〉,
〈(le‘ndx), ((𝐹
∘ 𝑁) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉} |
31 | | ssun2 3739 |
. . 3
⊢
{〈(TopSet‘ndx), (TopSet‘𝑈)〉, 〈(le‘ndx), ((𝐹 ∘ 𝑁) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}
⊆ (({〈(Base‘ndx), 𝐵〉, 〈(+g‘ndx),
(+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (TopSet‘𝑈)〉, 〈(le‘ndx), ((𝐹 ∘ 𝑁) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) |
32 | 30, 31 | sstri 3577 |
. 2
⊢
{〈(le‘ndx), ((𝐹 ∘ 𝑁) ∘ ◡𝐹)〉} ⊆ (({〈(Base‘ndx),
𝐵〉,
〈(+g‘ndx), (+g‘𝑈)〉, 〈(.r‘ndx),
(.r‘𝑈)〉} ∪ {〈(Scalar‘ndx),
(Scalar‘𝑅)〉,
〈( ·𝑠 ‘ndx), (
·𝑠 ‘𝑈)〉,
〈(·𝑖‘ndx), ∪ 𝑝 ∈ 𝑉 ∪ 𝑞 ∈ 𝑉 {〈〈(𝐹‘𝑝), (𝐹‘𝑞)〉, (𝑝(·𝑖‘𝑅)𝑞)〉}〉}) ∪
{〈(TopSet‘ndx), (TopSet‘𝑈)〉, 〈(le‘ndx), ((𝐹 ∘ 𝑁) ∘ ◡𝐹)〉, 〈(dist‘ndx),
(dist‘𝑈)〉}) |
33 | | fof 6028 |
. . . . . 6
⊢ (𝐹:𝑉–onto→𝐵 → 𝐹:𝑉⟶𝐵) |
34 | 12, 33 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:𝑉⟶𝐵) |
35 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑅)
∈ V |
36 | 2, 35 | syl6eqel 2696 |
. . . . 5
⊢ (𝜑 → 𝑉 ∈ V) |
37 | | fex 6394 |
. . . . 5
⊢ ((𝐹:𝑉⟶𝐵 ∧ 𝑉 ∈ V) → 𝐹 ∈ V) |
38 | 34, 36, 37 | syl2anc 691 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ V) |
39 | | fvex 6113 |
. . . . 5
⊢
(le‘𝑅) ∈
V |
40 | 11, 39 | eqeltri 2684 |
. . . 4
⊢ 𝑁 ∈ V |
41 | | coexg 7010 |
. . . 4
⊢ ((𝐹 ∈ V ∧ 𝑁 ∈ V) → (𝐹 ∘ 𝑁) ∈ V) |
42 | 38, 40, 41 | sylancl 693 |
. . 3
⊢ (𝜑 → (𝐹 ∘ 𝑁) ∈ V) |
43 | | cnvexg 7005 |
. . . 4
⊢ (𝐹 ∈ V → ◡𝐹 ∈ V) |
44 | 38, 43 | syl 17 |
. . 3
⊢ (𝜑 → ◡𝐹 ∈ V) |
45 | | coexg 7010 |
. . 3
⊢ (((𝐹 ∘ 𝑁) ∈ V ∧ ◡𝐹 ∈ V) → ((𝐹 ∘ 𝑁) ∘ ◡𝐹) ∈ V) |
46 | 42, 44, 45 | syl2anc 691 |
. 2
⊢ (𝜑 → ((𝐹 ∘ 𝑁) ∘ ◡𝐹) ∈ V) |
47 | | imasle.l |
. 2
⊢ ≤ =
(le‘𝑈) |
48 | 26, 28, 29, 32, 46, 47 | strfv3 15736 |
1
⊢ (𝜑 → ≤ = ((𝐹 ∘ 𝑁) ∘ ◡𝐹)) |