Step | Hyp | Ref
| Expression |
1 | | psrbas.s |
. . . . 5
β’ π = (πΌ mPwSer π
) |
2 | | psrbas.k |
. . . . 5
β’ πΎ = (Baseβπ
) |
3 | | eqid 2733 |
. . . . 5
β’
(+gβπ
) = (+gβπ
) |
4 | | eqid 2733 |
. . . . 5
β’
(.rβπ
) = (.rβπ
) |
5 | | eqid 2733 |
. . . . 5
β’
(TopOpenβπ
) =
(TopOpenβπ
) |
6 | | psrbas.d |
. . . . 5
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
7 | | eqidd 2734 |
. . . . 5
β’ ((π β§ π
β V) β (πΎ βm π·) = (πΎ βm π·)) |
8 | | eqid 2733 |
. . . . 5
β’ (
βf (+gβπ
) βΎ ((πΎ βm π·) Γ (πΎ βm π·))) = ( βf
(+gβπ
)
βΎ ((πΎ
βm π·)
Γ (πΎ
βm π·))) |
9 | | eqid 2733 |
. . . . 5
β’ (π β (πΎ βm π·), β β (πΎ βm π·) β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(ββ(π βf β π₯))))))) = (π β (πΎ βm π·), β β (πΎ βm π·) β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(ββ(π βf β π₯))))))) |
10 | | eqid 2733 |
. . . . 5
β’ (π₯ β πΎ, π β (πΎ βm π·) β¦ ((π· Γ {π₯}) βf
(.rβπ
)π)) = (π₯ β πΎ, π β (πΎ βm π·) β¦ ((π· Γ {π₯}) βf
(.rβπ
)π)) |
11 | | eqidd 2734 |
. . . . 5
β’ ((π β§ π
β V) β
(βtβ(π· Γ {(TopOpenβπ
)})) = (βtβ(π· Γ {(TopOpenβπ
)}))) |
12 | | psrbas.i |
. . . . . 6
β’ (π β πΌ β π) |
13 | 12 | adantr 482 |
. . . . 5
β’ ((π β§ π
β V) β πΌ β π) |
14 | | simpr 486 |
. . . . 5
β’ ((π β§ π
β V) β π
β V) |
15 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 13, 14 | psrval 21468 |
. . . 4
β’ ((π β§ π
β V) β π = ({β¨(Baseβndx), (πΎ βm π·)β©,
β¨(+gβndx), ( βf
(+gβπ
)
βΎ ((πΎ
βm π·)
Γ (πΎ
βm π·)))β©, β¨(.rβndx),
(π β (πΎ βm π·), β β (πΎ βm π·) β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(ββ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β (πΎ βm π·) β¦ ((π· Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©})) |
16 | 15 | fveq2d 6896 |
. . 3
β’ ((π β§ π
β V) β (Baseβπ) =
(Baseβ({β¨(Baseβndx), (πΎ βm π·)β©, β¨(+gβndx), (
βf (+gβπ
) βΎ ((πΎ βm π·) Γ (πΎ βm π·)))β©, β¨(.rβndx),
(π β (πΎ βm π·), β β (πΎ βm π·) β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(ββ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β (πΎ βm π·) β¦ ((π· Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}))) |
17 | | psrbas.b |
. . 3
β’ π΅ = (Baseβπ) |
18 | | ovex 7442 |
. . . 4
β’ (πΎ βm π·) β V |
19 | | psrvalstr 21469 |
. . . . 5
β’
({β¨(Baseβndx), (πΎ βm π·)β©, β¨(+gβndx), (
βf (+gβπ
) βΎ ((πΎ βm π·) Γ (πΎ βm π·)))β©, β¨(.rβndx),
(π β (πΎ βm π·), β β (πΎ βm π·) β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(ββ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β (πΎ βm π·) β¦ ((π· Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}) Struct β¨1,
9β© |
20 | | baseid 17147 |
. . . . 5
β’ Base =
Slot (Baseβndx) |
21 | | snsstp1 4820 |
. . . . . 6
β’
{β¨(Baseβndx), (πΎ βm π·)β©} β {β¨(Baseβndx),
(πΎ βm π·)β©,
β¨(+gβndx), ( βf
(+gβπ
)
βΎ ((πΎ
βm π·)
Γ (πΎ
βm π·)))β©, β¨(.rβndx),
(π β (πΎ βm π·), β β (πΎ βm π·) β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(ββ(π βf β π₯)))))))β©} |
22 | | ssun1 4173 |
. . . . . 6
β’
{β¨(Baseβndx), (πΎ βm π·)β©, β¨(+gβndx), (
βf (+gβπ
) βΎ ((πΎ βm π·) Γ (πΎ βm π·)))β©, β¨(.rβndx),
(π β (πΎ βm π·), β β (πΎ βm π·) β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(ββ(π βf β π₯)))))))β©} β
({β¨(Baseβndx), (πΎ βm π·)β©, β¨(+gβndx), (
βf (+gβπ
) βΎ ((πΎ βm π·) Γ (πΎ βm π·)))β©, β¨(.rβndx),
(π β (πΎ βm π·), β β (πΎ βm π·) β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(ββ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β (πΎ βm π·) β¦ ((π· Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}) |
23 | 21, 22 | sstri 3992 |
. . . . 5
β’
{β¨(Baseβndx), (πΎ βm π·)β©} β ({β¨(Baseβndx),
(πΎ βm π·)β©,
β¨(+gβndx), ( βf
(+gβπ
)
βΎ ((πΎ
βm π·)
Γ (πΎ
βm π·)))β©, β¨(.rβndx),
(π β (πΎ βm π·), β β (πΎ βm π·) β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(ββ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β (πΎ βm π·) β¦ ((π· Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}) |
24 | 19, 20, 23 | strfv 17137 |
. . . 4
β’ ((πΎ βm π·) β V β (πΎ βm π·) =
(Baseβ({β¨(Baseβndx), (πΎ βm π·)β©, β¨(+gβndx), (
βf (+gβπ
) βΎ ((πΎ βm π·) Γ (πΎ βm π·)))β©, β¨(.rβndx),
(π β (πΎ βm π·), β β (πΎ βm π·) β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(ββ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β (πΎ βm π·) β¦ ((π· Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}))) |
25 | 18, 24 | ax-mp 5 |
. . 3
β’ (πΎ βm π·) =
(Baseβ({β¨(Baseβndx), (πΎ βm π·)β©, β¨(+gβndx), (
βf (+gβπ
) βΎ ((πΎ βm π·) Γ (πΎ βm π·)))β©, β¨(.rβndx),
(π β (πΎ βm π·), β β (πΎ βm π·) β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(ββ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β (πΎ βm π·) β¦ ((π· Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©})) |
26 | 16, 17, 25 | 3eqtr4g 2798 |
. 2
β’ ((π β§ π
β V) β π΅ = (πΎ βm π·)) |
27 | | reldmpsr 21467 |
. . . . . . . 8
β’ Rel dom
mPwSer |
28 | 27 | ovprc2 7449 |
. . . . . . 7
β’ (Β¬
π
β V β (πΌ mPwSer π
) = β
) |
29 | 28 | adantl 483 |
. . . . . 6
β’ ((π β§ Β¬ π
β V) β (πΌ mPwSer π
) = β
) |
30 | 1, 29 | eqtrid 2785 |
. . . . 5
β’ ((π β§ Β¬ π
β V) β π = β
) |
31 | 30 | fveq2d 6896 |
. . . 4
β’ ((π β§ Β¬ π
β V) β (Baseβπ) =
(Baseββ
)) |
32 | | base0 17149 |
. . . 4
β’ β
=
(Baseββ
) |
33 | 31, 17, 32 | 3eqtr4g 2798 |
. . 3
β’ ((π β§ Β¬ π
β V) β π΅ = β
) |
34 | | fvprc 6884 |
. . . . . 6
β’ (Β¬
π
β V β
(Baseβπ
) =
β
) |
35 | 34 | adantl 483 |
. . . . 5
β’ ((π β§ Β¬ π
β V) β (Baseβπ
) = β
) |
36 | 2, 35 | eqtrid 2785 |
. . . 4
β’ ((π β§ Β¬ π
β V) β πΎ = β
) |
37 | 6 | fczpsrbag 21476 |
. . . . . . 7
β’ (πΌ β π β (π₯ β πΌ β¦ 0) β π·) |
38 | 12, 37 | syl 17 |
. . . . . 6
β’ (π β (π₯ β πΌ β¦ 0) β π·) |
39 | 38 | adantr 482 |
. . . . 5
β’ ((π β§ Β¬ π
β V) β (π₯ β πΌ β¦ 0) β π·) |
40 | 39 | ne0d 4336 |
. . . 4
β’ ((π β§ Β¬ π
β V) β π· β β
) |
41 | 2 | fvexi 6906 |
. . . . 5
β’ πΎ β V |
42 | | ovex 7442 |
. . . . . 6
β’
(β0 βm πΌ) β V |
43 | 6, 42 | rabex2 5335 |
. . . . 5
β’ π· β V |
44 | 41, 43 | map0 8881 |
. . . 4
β’ ((πΎ βm π·) = β
β (πΎ = β
β§ π· β β
)) |
45 | 36, 40, 44 | sylanbrc 584 |
. . 3
β’ ((π β§ Β¬ π
β V) β (πΎ βm π·) = β
) |
46 | 33, 45 | eqtr4d 2776 |
. 2
β’ ((π β§ Β¬ π
β V) β π΅ = (πΎ βm π·)) |
47 | 26, 46 | pm2.61dan 812 |
1
β’ (π β π΅ = (πΎ βm π·)) |