Step | Hyp | Ref
| Expression |
1 | | imasbas.u |
. . 3
β’ (π β π = (πΉ βs π
)) |
2 | | imasbas.v |
. . 3
β’ (π β π = (Baseβπ
)) |
3 | | eqid 2737 |
. . 3
β’
(+gβπ
) = (+gβπ
) |
4 | | eqid 2737 |
. . 3
β’
(.rβπ
) = (.rβπ
) |
5 | | eqid 2737 |
. . 3
β’
(Scalarβπ
) =
(Scalarβπ
) |
6 | | eqid 2737 |
. . 3
β’
(Baseβ(Scalarβπ
)) = (Baseβ(Scalarβπ
)) |
7 | | eqid 2737 |
. . 3
β’ (
Β·π βπ
) = ( Β·π
βπ
) |
8 | | eqid 2737 |
. . 3
β’
(Β·πβπ
) =
(Β·πβπ
) |
9 | | eqid 2737 |
. . 3
β’
(TopOpenβπ
) =
(TopOpenβπ
) |
10 | | eqid 2737 |
. . 3
β’
(distβπ
) =
(distβπ
) |
11 | | imasle.n |
. . 3
β’ π = (leβπ
) |
12 | | imasbas.f |
. . . 4
β’ (π β πΉ:πβontoβπ΅) |
13 | | imasbas.r |
. . . 4
β’ (π β π
β π) |
14 | | eqid 2737 |
. . . 4
β’
(+gβπ) = (+gβπ) |
15 | 1, 2, 12, 13, 3, 14 | imasplusg 17400 |
. . 3
β’ (π β (+gβπ) = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(+gβπ
)π))β©}) |
16 | | eqid 2737 |
. . . 4
β’
(.rβπ) = (.rβπ) |
17 | 1, 2, 12, 13, 4, 16 | imasmulr 17401 |
. . 3
β’ (π β (.rβπ) = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}) |
18 | | eqid 2737 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
19 | 1, 2, 12, 13, 5, 6, 7, 18 | imasvsca 17403 |
. . 3
β’ (π β (
Β·π βπ) = βͺ
π β π (π β (Baseβ(Scalarβπ
)), π₯ β {(πΉβπ)} β¦ (πΉβ(π( Β·π
βπ
)π)))) |
20 | | eqidd 2738 |
. . 3
β’ (π β βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©} = βͺ
π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©}) |
21 | | eqid 2737 |
. . . 4
β’
(TopSetβπ) =
(TopSetβπ) |
22 | 1, 2, 12, 13, 9, 21 | imastset 17405 |
. . 3
β’ (π β (TopSetβπ) = ((TopOpenβπ
) qTop πΉ)) |
23 | | eqid 2737 |
. . . 4
β’
(distβπ) =
(distβπ) |
24 | 1, 2, 12, 13, 10, 23 | imasds 17396 |
. . 3
β’ (π β (distβπ) = (π₯ β π΅, π¦ β π΅ β¦ inf(βͺ π’ β β ran (π§ β {π€ β ((π Γ π) βm (1...π’)) β£ ((πΉβ(1st β(π€β1))) = π₯ β§ (πΉβ(2nd β(π€βπ’))) = π¦ β§ βπ£ β (1...(π’ β 1))(πΉβ(2nd β(π€βπ£))) = (πΉβ(1st β(π€β(π£ + 1)))))} β¦
(β*π Ξ£g
((distβπ
) β
π§))), β*,
< ))) |
25 | | eqidd 2738 |
. . 3
β’ (π β ((πΉ β π) β β‘πΉ) = ((πΉ β π) β β‘πΉ)) |
26 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 15, 17, 19, 20, 22, 24, 25, 12, 13 | imasval 17394 |
. 2
β’ (π β π = (({β¨(Baseβndx), π΅β©,
β¨(+gβndx), (+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
(Scalarβπ
)β©,
β¨( Β·π βndx), (
Β·π βπ)β©,
β¨(Β·πβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©}β©}) βͺ
{β¨(TopSetβndx), (TopSetβπ)β©, β¨(leβndx), ((πΉ β π) β β‘πΉ)β©, β¨(distβndx),
(distβπ)β©})) |
27 | | eqid 2737 |
. . 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 17334 |
. 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 17249 |
. 2
β’ le = Slot
(leβndx) |
30 | | snsstp2 4778 |
. . 3
β’
{β¨(leβndx), ((πΉ β π) β β‘πΉ)β©} β {β¨(TopSetβndx),
(TopSetβπ)β©,
β¨(leβndx), ((πΉ
β π) β β‘πΉ)β©, β¨(distβndx),
(distβπ)β©} |
31 | | ssun2 4134 |
. . 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 3954 |
. 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 6757 |
. . . . . 6
β’ (πΉ:πβontoβπ΅ β πΉ:πβΆπ΅) |
34 | 12, 33 | syl 17 |
. . . . 5
β’ (π β πΉ:πβΆπ΅) |
35 | | fvex 6856 |
. . . . . 6
β’
(Baseβπ
)
β V |
36 | 2, 35 | eqeltrdi 2846 |
. . . . 5
β’ (π β π β V) |
37 | 34, 36 | fexd 7178 |
. . . 4
β’ (π β πΉ β V) |
38 | 11 | fvexi 6857 |
. . . 4
β’ π β V |
39 | | coexg 7867 |
. . . 4
β’ ((πΉ β V β§ π β V) β (πΉ β π) β V) |
40 | 37, 38, 39 | sylancl 587 |
. . 3
β’ (π β (πΉ β π) β V) |
41 | | cnvexg 7862 |
. . . 4
β’ (πΉ β V β β‘πΉ β V) |
42 | 37, 41 | syl 17 |
. . 3
β’ (π β β‘πΉ β V) |
43 | | coexg 7867 |
. . 3
β’ (((πΉ β π) β V β§ β‘πΉ β V) β ((πΉ β π) β β‘πΉ) β V) |
44 | 40, 42, 43 | syl2anc 585 |
. 2
β’ (π β ((πΉ β π) β β‘πΉ) β V) |
45 | | imasle.l |
. 2
β’ β€ =
(leβπ) |
46 | 26, 28, 29, 32, 44, 45 | strfv3 17078 |
1
β’ (π β β€ = ((πΉ β π) β β‘πΉ)) |