Step | Hyp | Ref
| Expression |
1 | | prdsbas.p |
. . 3
β’ π = (πXsπ
) |
2 | | eqid 2733 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
3 | | prdsbas.i |
. . 3
β’ (π β dom π
= πΌ) |
4 | | eqidd 2734 |
. . 3
β’ (π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)) = Xπ₯ β πΌ (Baseβ(π
βπ₯))) |
5 | | eqidd 2734 |
. . 3
β’ (π β (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π
βπ₯))(πβπ₯)))) = (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π
βπ₯))(πβπ₯))))) |
6 | | eqidd 2734 |
. . 3
β’ (π β (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)))) = (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))) |
7 | | eqidd 2734 |
. . 3
β’ (π β (π β (Baseβπ), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯)))) = (π β (Baseβπ), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))) |
8 | | eqidd 2734 |
. . 3
β’ (π β (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯))))) = (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))) |
9 | | eqidd 2734 |
. . 3
β’ (π β
(βtβ(TopOpen β π
)) = (βtβ(TopOpen
β π
))) |
10 | | eqidd 2734 |
. . 3
β’ (π β {β¨π, πβ© β£ ({π, π} β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))} = {β¨π, πβ© β£ ({π, π} β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))}) |
11 | | eqidd 2734 |
. . 3
β’ (π β (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, < ))
= (π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))) |
12 | | eqidd 2734 |
. . 3
β’ (π β (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯))) = (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))) |
13 | | eqidd 2734 |
. . 3
β’ (π β (π β (Xπ₯ β πΌ (Baseβ(π
βπ₯)) Γ Xπ₯ β πΌ (Baseβ(π
βπ₯))), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π β ((2nd βπ)(π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯))))) = (π β (Xπ₯ β πΌ (Baseβ(π
βπ₯)) Γ Xπ₯ β πΌ (Baseβ(π
βπ₯))), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π β ((2nd βπ)(π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))) |
14 | | prdsbas.s |
. . 3
β’ (π β π β π) |
15 | | prdsbas.r |
. . 3
β’ (π β π
β π) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15 | prdsval 17342 |
. 2
β’ (π β π = (({β¨(Baseβndx), Xπ₯ β
πΌ (Baseβ(π
βπ₯))β©, β¨(+gβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π
βπ₯))(πβπ₯))))β©, β¨(.rβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π β (Baseβπ), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(βtβ(TopOpen β π
))β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))}β©, β¨(distβndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (Xπ₯ β πΌ (Baseβ(π
βπ₯)) Γ Xπ₯ β πΌ (Baseβ(π
βπ₯))), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π β ((2nd βπ)(π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©}))) |
17 | | prdsbas.b |
. 2
β’ π΅ = (Baseβπ) |
18 | | baseid 17091 |
. 2
β’ Base =
Slot (Baseβndx) |
19 | 18 | strfvss 17064 |
. . . . . . 7
β’
(Baseβ(π
βπ₯)) β βͺ ran
(π
βπ₯) |
20 | | fvssunirn 6876 |
. . . . . . . 8
β’ (π
βπ₯) β βͺ ran
π
|
21 | | rnss 5895 |
. . . . . . . 8
β’ ((π
βπ₯) β βͺ ran
π
β ran (π
βπ₯) β ran βͺ
ran π
) |
22 | | uniss 4874 |
. . . . . . . 8
β’ (ran
(π
βπ₯) β ran βͺ
ran π
β βͺ ran (π
βπ₯) β βͺ ran
βͺ ran π
) |
23 | 20, 21, 22 | mp2b 10 |
. . . . . . 7
β’ βͺ ran (π
βπ₯) β βͺ ran
βͺ ran π
|
24 | 19, 23 | sstri 3954 |
. . . . . 6
β’
(Baseβ(π
βπ₯)) β βͺ ran
βͺ ran π
|
25 | 24 | rgenw 3065 |
. . . . 5
β’
βπ₯ β
πΌ (Baseβ(π
βπ₯)) β βͺ ran
βͺ ran π
|
26 | | iunss 5006 |
. . . . 5
β’ (βͺ π₯ β πΌ (Baseβ(π
βπ₯)) β βͺ ran
βͺ ran π
β βπ₯ β πΌ (Baseβ(π
βπ₯)) β βͺ ran
βͺ ran π
) |
27 | 25, 26 | mpbir 230 |
. . . 4
β’ βͺ π₯ β πΌ (Baseβ(π
βπ₯)) β βͺ ran
βͺ ran π
|
28 | | rnexg 7842 |
. . . . . 6
β’ (π
β π β ran π
β V) |
29 | | uniexg 7678 |
. . . . . 6
β’ (ran
π
β V β βͺ ran π
β V) |
30 | 15, 28, 29 | 3syl 18 |
. . . . 5
β’ (π β βͺ ran π
β V) |
31 | | rnexg 7842 |
. . . . 5
β’ (βͺ ran π
β V β ran βͺ ran π
β V) |
32 | | uniexg 7678 |
. . . . 5
β’ (ran
βͺ ran π
β V β βͺ ran βͺ ran π
β V) |
33 | 30, 31, 32 | 3syl 18 |
. . . 4
β’ (π β βͺ ran βͺ ran π
β V) |
34 | | ssexg 5281 |
. . . 4
β’
((βͺ π₯ β πΌ (Baseβ(π
βπ₯)) β βͺ ran
βͺ ran π
β§ βͺ ran
βͺ ran π
β V) β βͺ π₯ β πΌ (Baseβ(π
βπ₯)) β V) |
35 | 27, 33, 34 | sylancr 588 |
. . 3
β’ (π β βͺ π₯ β πΌ (Baseβ(π
βπ₯)) β V) |
36 | | ixpssmap2g 8868 |
. . 3
β’ (βͺ π₯ β πΌ (Baseβ(π
βπ₯)) β V β Xπ₯ β
πΌ (Baseβ(π
βπ₯)) β (βͺ π₯ β πΌ (Baseβ(π
βπ₯)) βm πΌ)) |
37 | | ovex 7391 |
. . . 4
β’ (βͺ π₯ β πΌ (Baseβ(π
βπ₯)) βm πΌ) β V |
38 | 37 | ssex 5279 |
. . 3
β’ (Xπ₯ β
πΌ (Baseβ(π
βπ₯)) β (βͺ π₯ β πΌ (Baseβ(π
βπ₯)) βm πΌ) β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β V) |
39 | 35, 36, 38 | 3syl 18 |
. 2
β’ (π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)) β V) |
40 | | snsstp1 4777 |
. . . 4
β’
{β¨(Baseβndx), Xπ₯ β πΌ (Baseβ(π
βπ₯))β©} β {β¨(Baseβndx),
Xπ₯
β πΌ (Baseβ(π
βπ₯))β©, β¨(+gβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π
βπ₯))(πβπ₯))))β©, β¨(.rβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} |
41 | | ssun1 4133 |
. . . 4
β’
{β¨(Baseβndx), Xπ₯ β πΌ (Baseβ(π
βπ₯))β©, β¨(+gβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π
βπ₯))(πβπ₯))))β©, β¨(.rβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} β ({β¨(Baseβndx),
Xπ₯
β πΌ (Baseβ(π
βπ₯))β©, β¨(+gβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π
βπ₯))(πβπ₯))))β©, β¨(.rβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π β (Baseβπ), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) |
42 | 40, 41 | sstri 3954 |
. . 3
β’
{β¨(Baseβndx), Xπ₯ β πΌ (Baseβ(π
βπ₯))β©} β ({β¨(Baseβndx),
Xπ₯
β πΌ (Baseβ(π
βπ₯))β©, β¨(+gβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π
βπ₯))(πβπ₯))))β©, β¨(.rβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π β (Baseβπ), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) |
43 | | ssun1 4133 |
. . 3
β’
({β¨(Baseβndx), Xπ₯ β πΌ (Baseβ(π
βπ₯))β©, β¨(+gβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π
βπ₯))(πβπ₯))))β©, β¨(.rβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π β (Baseβπ), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) β (({β¨(Baseβndx),
Xπ₯ β
πΌ (Baseβ(π
βπ₯))β©, β¨(+gβndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π
βπ₯))(πβπ₯))))β©, β¨(.rβndx),
(π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), (π β (Baseβπ), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(βtβ(TopOpen β π
))β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))}β©, β¨(distβndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (Xπ₯ β πΌ (Baseβ(π
βπ₯)) Γ Xπ₯ β πΌ (Baseβ(π
βπ₯))), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π β ((2nd βπ)(π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©})) |
44 | 42, 43 | sstri 3954 |
. 2
β’
{β¨(Baseβndx), Xπ₯ β πΌ (Baseβ(π
βπ₯))β©} β (({β¨(Baseβndx),
Xπ₯
β πΌ (Baseβ(π
βπ₯))β©, β¨(+gβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π
βπ₯))(πβπ₯))))β©, β¨(.rβndx),
(π β Xπ₯ β
πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π β (Baseβπ), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(βtβ(TopOpen β π
))β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))}β©, β¨(distβndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), (π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (Xπ₯ β πΌ (Baseβ(π
βπ₯)) Γ Xπ₯ β πΌ (Baseβ(π
βπ₯))), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ (π β ((2nd βπ)(π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β Xπ₯ β πΌ (Baseβ(π
βπ₯)), π β Xπ₯ β πΌ (Baseβ(π
βπ₯)) β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©})) |
45 | 16, 17, 18, 39, 44 | prdsbaslem 17340 |
1
β’ (π β π΅ = Xπ₯ β πΌ (Baseβ(π
βπ₯))) |