Step | Hyp | Ref
| Expression |
1 | | imasbas.u |
. . 3
β’ (π β π = (πΉ βs π
)) |
2 | | imasbas.v |
. . 3
β’ (π β π = (Baseβπ
)) |
3 | | imasplusg.p |
. . 3
β’ + =
(+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 | | eqid 2737 |
. . 3
β’
(leβπ
) =
(leβπ
) |
12 | | eqidd 2738 |
. . 3
β’ (π β βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©} = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}) |
13 | | eqidd 2738 |
. . 3
β’ (π β βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©} = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}) |
14 | | eqidd 2738 |
. . 3
β’ (π β βͺ π β π (π β (Baseβ(Scalarβπ
)), π₯ β {(πΉβπ)} β¦ (πΉβ(π( Β·π
βπ
)π))) = βͺ
π β π (π β (Baseβ(Scalarβπ
)), π₯ β {(πΉβπ)} β¦ (πΉβ(π( Β·π
βπ
)π)))) |
15 | | eqidd 2738 |
. . 3
β’ (π β βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©} = βͺ
π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©}) |
16 | | eqidd 2738 |
. . 3
β’ (π β ((TopOpenβπ
) qTop πΉ) = ((TopOpenβπ
) qTop πΉ)) |
17 | | imasbas.f |
. . . 4
β’ (π β πΉ:πβontoβπ΅) |
18 | | imasbas.r |
. . . 4
β’ (π β π
β π) |
19 | | eqid 2737 |
. . . 4
β’
(distβπ) =
(distβπ) |
20 | 1, 2, 17, 18, 10, 19 | imasds 17396 |
. . 3
β’ (π β (distβπ) = (π₯ β π΅, π¦ β π΅ β¦ inf(βͺ π β β ran (π β {β β ((π Γ π) βm (1...π)) β£ ((πΉβ(1st β(ββ1))) = π₯ β§ (πΉβ(2nd β(ββπ))) = π¦ β§ βπ β (1...(π β 1))(πΉβ(2nd β(ββπ))) = (πΉβ(1st β(ββ(π + 1)))))} β¦
(β*π Ξ£g
((distβπ
) β
π))), β*,
< ))) |
21 | | eqidd 2738 |
. . 3
β’ (π β ((πΉ β (leβπ
)) β β‘πΉ) = ((πΉ β (leβπ
)) β β‘πΉ)) |
22 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 20, 21, 17, 18 | imasval 17394 |
. 2
β’ (π β π = (({β¨(Baseβndx), π΅β©,
β¨(+gβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©,
β¨(.rβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}β©} βͺ
{β¨(Scalarβndx), (Scalarβπ
)β©, β¨(
Β·π βndx), βͺ π β π (π β (Baseβ(Scalarβπ
)), π₯ β {(πΉβπ)} β¦ (πΉβ(π( Β·π
βπ
)π)))β©,
β¨(Β·πβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©}β©}) βͺ
{β¨(TopSetβndx), ((TopOpenβπ
) qTop πΉ)β©, β¨(leβndx), ((πΉ β (leβπ
)) β β‘πΉ)β©, β¨(distβndx),
(distβπ)β©})) |
23 | | eqid 2737 |
. . 3
β’
(({β¨(Baseβndx), π΅β©, β¨(+gβndx),
βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©,
β¨(.rβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}β©} βͺ
{β¨(Scalarβndx), (Scalarβπ
)β©, β¨(
Β·π βndx), βͺ π β π (π β (Baseβ(Scalarβπ
)), π₯ β {(πΉβπ)} β¦ (πΉβ(π( Β·π
βπ
)π)))β©,
β¨(Β·πβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©}β©}) βͺ
{β¨(TopSetβndx), ((TopOpenβπ
) qTop πΉ)β©, β¨(leβndx), ((πΉ β (leβπ
)) β β‘πΉ)β©, β¨(distβndx),
(distβπ)β©}) =
(({β¨(Baseβndx), π΅β©, β¨(+gβndx),
βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©,
β¨(.rβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}β©} βͺ
{β¨(Scalarβndx), (Scalarβπ
)β©, β¨(
Β·π βndx), βͺ π
β π (π β (Baseβ(Scalarβπ
)), π₯ β {(πΉβπ)} β¦ (πΉβ(π( Β·π
βπ
)π)))β©,
β¨(Β·πβndx), βͺ π
β π βͺ π
β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©}β©}) βͺ
{β¨(TopSetβndx), ((TopOpenβπ
) qTop πΉ)β©, β¨(leβndx), ((πΉ β (leβπ
)) β β‘πΉ)β©, β¨(distβndx),
(distβπ)β©}) |
24 | 23 | imasvalstr 17334 |
. 2
β’
(({β¨(Baseβndx), π΅β©, β¨(+gβndx),
βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©,
β¨(.rβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}β©} βͺ
{β¨(Scalarβndx), (Scalarβπ
)β©, β¨(
Β·π βndx), βͺ π β π (π β (Baseβ(Scalarβπ
)), π₯ β {(πΉβπ)} β¦ (πΉβ(π( Β·π
βπ
)π)))β©,
β¨(Β·πβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©}β©}) βͺ
{β¨(TopSetβndx), ((TopOpenβπ
) qTop πΉ)β©, β¨(leβndx), ((πΉ β (leβπ
)) β β‘πΉ)β©, β¨(distβndx),
(distβπ)β©}) Struct
β¨1, ;12β© |
25 | | plusgid 17161 |
. 2
β’
+g = Slot (+gβndx) |
26 | | snsstp2 4778 |
. . . 4
β’
{β¨(+gβndx), βͺ
π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©} β
{β¨(Baseβndx), π΅β©, β¨(+gβndx),
βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©,
β¨(.rβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}β©} |
27 | | ssun1 4133 |
. . . 4
β’
{β¨(Baseβndx), π΅β©, β¨(+gβndx),
βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©,
β¨(.rβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}β©} β
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©,
β¨(.rβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}β©} βͺ
{β¨(Scalarβndx), (Scalarβπ
)β©, β¨(
Β·π βndx), βͺ π β π (π β (Baseβ(Scalarβπ
)), π₯ β {(πΉβπ)} β¦ (πΉβ(π( Β·π
βπ
)π)))β©,
β¨(Β·πβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©}β©}) |
28 | 26, 27 | sstri 3954 |
. . 3
β’
{β¨(+gβndx), βͺ
π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©} β
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©,
β¨(.rβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}β©} βͺ
{β¨(Scalarβndx), (Scalarβπ
)β©, β¨(
Β·π βndx), βͺ π β π (π β (Baseβ(Scalarβπ
)), π₯ β {(πΉβπ)} β¦ (πΉβ(π( Β·π
βπ
)π)))β©,
β¨(Β·πβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©}β©}) |
29 | | ssun1 4133 |
. . 3
β’
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©,
β¨(.rβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}β©} βͺ
{β¨(Scalarβndx), (Scalarβπ
)β©, β¨(
Β·π βndx), βͺ π β π (π β (Baseβ(Scalarβπ
)), π₯ β {(πΉβπ)} β¦ (πΉβ(π( Β·π
βπ
)π)))β©,
β¨(Β·πβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©}β©}) β
(({β¨(Baseβndx), π΅β©, β¨(+gβndx),
βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©,
β¨(.rβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}β©} βͺ
{β¨(Scalarβndx), (Scalarβπ
)β©, β¨(
Β·π βndx), βͺ π
β π (π β (Baseβ(Scalarβπ
)), π₯ β {(πΉβπ)} β¦ (πΉβ(π( Β·π
βπ
)π)))β©,
β¨(Β·πβndx), βͺ π
β π βͺ π
β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©}β©}) βͺ
{β¨(TopSetβndx), ((TopOpenβπ
) qTop πΉ)β©, β¨(leβndx), ((πΉ β (leβπ
)) β β‘πΉ)β©, β¨(distβndx),
(distβπ)β©}) |
30 | 28, 29 | sstri 3954 |
. 2
β’
{β¨(+gβndx), βͺ
π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©} β
(({β¨(Baseβndx), π΅β©, β¨(+gβndx),
βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}β©,
β¨(.rβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π(.rβπ
)π))β©}β©} βͺ
{β¨(Scalarβndx), (Scalarβπ
)β©, β¨(
Β·π βndx), βͺ π β π (π β (Baseβ(Scalarβπ
)), π₯ β {(πΉβπ)} β¦ (πΉβ(π( Β·π
βπ
)π)))β©,
β¨(Β·πβndx), βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (π(Β·πβπ
)π)β©}β©}) βͺ
{β¨(TopSetβndx), ((TopOpenβπ
) qTop πΉ)β©, β¨(leβndx), ((πΉ β (leβπ
)) β β‘πΉ)β©, β¨(distβndx),
(distβπ)β©}) |
31 | | fvex 6856 |
. . . 4
β’
(Baseβπ
)
β V |
32 | 2, 31 | eqeltrdi 2846 |
. . 3
β’ (π β π β V) |
33 | | snex 5389 |
. . . . . 6
β’
{β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©} β V |
34 | 33 | rgenw 3069 |
. . . . 5
β’
βπ β
π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©} β V |
35 | | iunexg 7897 |
. . . . 5
β’ ((π β V β§ βπ β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©} β V) β βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©} β V) |
36 | 32, 34, 35 | sylancl 587 |
. . . 4
β’ (π β βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©} β V) |
37 | 36 | ralrimivw 3148 |
. . 3
β’ (π β βπ β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©} β V) |
38 | | iunexg 7897 |
. . 3
β’ ((π β V β§ βπ β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©} β V) β βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©} β V) |
39 | 32, 37, 38 | syl2anc 585 |
. 2
β’ (π β βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©} β V) |
40 | | imasplusg.a |
. 2
β’ β =
(+gβπ) |
41 | 22, 24, 25, 30, 39, 40 | strfv3 17078 |
1
β’ (π β β = βͺ π β π βͺ π β π {β¨β¨(πΉβπ), (πΉβπ)β©, (πΉβ(π + π))β©}) |