Step | Hyp | Ref
| Expression |
1 | | prdsbas.p |
. . 3
β’ π = (πXsπ
) |
2 | | eqid 2737 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
3 | | prdsbas.i |
. . 3
β’ (π β dom π
= πΌ) |
4 | | prdsbas.s |
. . . 4
β’ (π β π β π) |
5 | | prdsbas.r |
. . . 4
β’ (π β π
β π) |
6 | | prdsbas.b |
. . . 4
β’ π΅ = (Baseβπ) |
7 | 1, 4, 5, 6, 3 | prdsbas 17346 |
. . 3
β’ (π β π΅ = Xπ₯ β πΌ (Baseβ(π
βπ₯))) |
8 | | eqid 2737 |
. . . 4
β’
(+gβπ) = (+gβπ) |
9 | 1, 4, 5, 6, 3, 8 | prdsplusg 17347 |
. . 3
β’ (π β (+gβπ) = (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π
βπ₯))(πβπ₯))))) |
10 | | eqid 2737 |
. . . 4
β’
(.rβπ) = (.rβπ) |
11 | 1, 4, 5, 6, 3, 10 | prdsmulr 17348 |
. . 3
β’ (π β (.rβπ) = (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))) |
12 | | eqid 2737 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
13 | 1, 4, 5, 6, 3, 2, 12 | prdsvsca 17349 |
. . 3
β’ (π β (
Β·π βπ) = (π β (Baseβπ), π β π΅ β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))) |
14 | | eqidd 2738 |
. . 3
β’ (π β (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯))))) = (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))) |
15 | | eqidd 2738 |
. . 3
β’ (π β
(βtβ(TopOpen β π
)) = (βtβ(TopOpen
β π
))) |
16 | | eqid 2737 |
. . . 4
β’
(leβπ) =
(leβπ) |
17 | 1, 4, 5, 6, 3, 16 | prdsle 17351 |
. . 3
β’ (π β (leβπ) = {β¨π, πβ© β£ ({π, π} β π΅ β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))}) |
18 | | eqidd 2738 |
. . 3
β’ (π β (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, < ))
= (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))) |
19 | | eqidd 2738 |
. . 3
β’ (π β (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯))) = (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))) |
20 | | eqidd 2738 |
. . 3
β’ (π β (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯))))) = (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))) |
21 | 1, 2, 3, 7, 9, 11,
13, 14, 15, 17, 18, 19, 20, 4, 5 | prdsval 17344 |
. 2
β’ (π β π = (({β¨(Baseβndx), π΅β©,
β¨(+gβndx), (+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (
Β·π βπ)β©,
β¨(Β·πβndx), (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(βtβ(TopOpen β π
))β©, β¨(leβndx), (leβπ)β©, β¨(distβndx),
(π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©}))) |
22 | | prdsds.l |
. 2
β’ π· = (distβπ) |
23 | | dsid 17274 |
. 2
β’ dist =
Slot (distβndx) |
24 | 6 | fvexi 6861 |
. . . 4
β’ π΅ β V |
25 | | xrex 12919 |
. . . . . 6
β’
β* β V |
26 | 25 | uniex 7683 |
. . . . 5
β’ βͺ β* β V |
27 | 26 | pwex 5340 |
. . . 4
β’ π«
βͺ β* β V |
28 | | df-sup 9385 |
. . . . . 6
β’ sup((ran
(π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, < ) =
βͺ {π¦ β β* β£
(βπ§ β (ran
(π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}) Β¬ π¦ < π§ β§ βπ§ β β* (π§ < π¦ β βπ€ β (ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0})π§ < π€))} |
29 | | ssrab2 4042 |
. . . . . . . 8
β’ {π¦ β β*
β£ (βπ§ β
(ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}) Β¬ π¦ < π§ β§ βπ§ β β* (π§ < π¦ β βπ€ β (ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0})π§ < π€))} β
β* |
30 | 29 | unissi 4879 |
. . . . . . 7
β’ βͺ {π¦
β β* β£ (βπ§ β (ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}) Β¬ π¦ < π§ β§ βπ§ β β* (π§ < π¦ β βπ€ β (ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0})π§ < π€))} β βͺ
β* |
31 | 26, 30 | elpwi2 5308 |
. . . . . 6
β’ βͺ {π¦
β β* β£ (βπ§ β (ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}) Β¬ π¦ < π§ β§ βπ§ β β* (π§ < π¦ β βπ€ β (ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0})π§ < π€))} β π« βͺ β* |
32 | 28, 31 | eqeltri 2834 |
. . . . 5
β’ sup((ran
(π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, < )
β π« βͺ
β* |
33 | 32 | rgen2w 3070 |
. . . 4
β’
βπ β
π΅ βπ β π΅ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, < )
β π« βͺ
β* |
34 | 24, 24, 27, 33 | mpoexw 8016 |
. . 3
β’ (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, < ))
β V |
35 | 34 | a1i 11 |
. 2
β’ (π β (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, < ))
β V) |
36 | | snsstp3 4783 |
. . . 4
β’
{β¨(distβndx), (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} β {β¨(TopSetβndx), (βtβ(TopOpen
β π
))β©,
β¨(leβndx), (leβπ)β©, β¨(distβndx), (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} |
37 | | ssun1 4137 |
. . . 4
β’
{β¨(TopSetβndx), (βtβ(TopOpen β
π
))β©,
β¨(leβndx), (leβπ)β©, β¨(distβndx), (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} β ({β¨(TopSetβndx),
(βtβ(TopOpen β π
))β©, β¨(leβndx),
(leβπ)β©,
β¨(distβndx), (π
β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©}) |
38 | 36, 37 | sstri 3958 |
. . 3
β’
{β¨(distβndx), (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} β ({β¨(TopSetβndx),
(βtβ(TopOpen β π
))β©, β¨(leβndx),
(leβπ)β©,
β¨(distβndx), (π
β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©}) |
39 | | ssun2 4138 |
. . 3
β’
({β¨(TopSetβndx), (βtβ(TopOpen β
π
))β©,
β¨(leβndx), (leβπ)β©, β¨(distβndx), (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©}) β
(({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (
Β·π βπ)β©,
β¨(Β·πβndx), (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(βtβ(TopOpen β π
))β©, β¨(leβndx), (leβπ)β©, β¨(distβndx),
(π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©})) |
40 | 38, 39 | sstri 3958 |
. 2
β’
{β¨(distβndx), (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} β (({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (
Β·π βπ)β©,
β¨(Β·πβndx), (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(βtβ(TopOpen β π
))β©, β¨(leβndx), (leβπ)β©, β¨(distβndx),
(π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©})) |
41 | 21, 22, 23, 35, 40 | prdsbaslem 17342 |
1
β’ (π β π· = (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))) |