Step | Hyp | Ref
| Expression |
1 | | psrplusg.s |
. . . . 5
β’ π = (πΌ mPwSer π
) |
2 | | eqid 2733 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
3 | | psrplusg.a |
. . . . 5
β’ + =
(+gβπ
) |
4 | | eqid 2733 |
. . . . 5
β’
(.rβπ
) = (.rβπ
) |
5 | | eqid 2733 |
. . . . 5
β’
(TopOpenβπ
) =
(TopOpenβπ
) |
6 | | eqid 2733 |
. . . . 5
β’ {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
7 | | psrplusg.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
8 | | simpl 484 |
. . . . . 6
β’ ((πΌ β V β§ π
β V) β πΌ β V) |
9 | 1, 2, 6, 7, 8 | psrbas 21362 |
. . . . 5
β’ ((πΌ β V β§ π
β V) β π΅ = ((Baseβπ
) βm {β β (β0
βm πΌ)
β£ (β‘β β β) β
Fin})) |
10 | | eqid 2733 |
. . . . 5
β’ (
βf + βΎ (π΅ Γ π΅)) = ( βf + βΎ
(π΅ Γ π΅)) |
11 | | eqid 2733 |
. . . . 5
β’ (π β π΅, π β π΅ β¦ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯))))))) = (π β π΅, π β π΅ β¦ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯))))))) |
12 | | eqid 2733 |
. . . . 5
β’ (π₯ β (Baseβπ
), π β π΅ β¦ (({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ {π₯}) βf
(.rβπ
)π)) = (π₯ β (Baseβπ
), π β π΅ β¦ (({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ {π₯}) βf
(.rβπ
)π)) |
13 | | eqidd 2734 |
. . . . 5
β’ ((πΌ β V β§ π
β V) β
(βtβ({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ
{(TopOpenβπ
)})) =
(βtβ({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ
{(TopOpenβπ
)}))) |
14 | | simpr 486 |
. . . . 5
β’ ((πΌ β V β§ π
β V) β π
β V) |
15 | 1, 2, 3, 4, 5, 6, 9, 10, 11, 12, 13, 8, 14 | psrval 21333 |
. . . 4
β’ ((πΌ β V β§ π
β V) β π = ({β¨(Baseβndx),
π΅β©,
β¨(+gβndx), ( βf + βΎ (π΅ Γ π΅))β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ (({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ
{(TopOpenβπ
)}))β©})) |
16 | 15 | fveq2d 6847 |
. . 3
β’ ((πΌ β V β§ π
β V) β
(+gβπ) =
(+gβ({β¨(Baseβndx), π΅β©, β¨(+gβndx), (
βf + βΎ (π΅ Γ π΅))β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ (({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ
{(TopOpenβπ
)}))β©}))) |
17 | | psrplusg.p |
. . 3
β’ β =
(+gβπ) |
18 | 7 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
19 | 18, 18 | xpex 7688 |
. . . 4
β’ (π΅ Γ π΅) β V |
20 | | ofexg 7623 |
. . . 4
β’ ((π΅ Γ π΅) β V β ( βf
+ βΎ
(π΅ Γ π΅)) β V) |
21 | | psrvalstr 21334 |
. . . . 5
β’
({β¨(Baseβndx), π΅β©, β¨(+gβndx), (
βf + βΎ (π΅ Γ π΅))β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ (({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ
{(TopOpenβπ
)}))β©}) Struct β¨1,
9β© |
22 | | plusgid 17165 |
. . . . 5
β’
+g = Slot (+gβndx) |
23 | | snsstp2 4778 |
. . . . . 6
β’
{β¨(+gβndx), ( βf + βΎ
(π΅ Γ π΅))β©} β
{β¨(Baseβndx), π΅β©, β¨(+gβndx), (
βf + βΎ (π΅ Γ π΅))β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))))β©} |
24 | | ssun1 4133 |
. . . . . 6
β’
{β¨(Baseβndx), π΅β©, β¨(+gβndx), (
βf + βΎ (π΅ Γ π΅))β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))))β©} β
({β¨(Baseβndx), π΅β©, β¨(+gβndx), (
βf + βΎ (π΅ Γ π΅))β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ (({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ
{(TopOpenβπ
)}))β©}) |
25 | 23, 24 | sstri 3954 |
. . . . 5
β’
{β¨(+gβndx), ( βf + βΎ
(π΅ Γ π΅))β©} β
({β¨(Baseβndx), π΅β©, β¨(+gβndx), (
βf + βΎ (π΅ Γ π΅))β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ (({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ
{(TopOpenβπ
)}))β©}) |
26 | 21, 22, 25 | strfv 17081 |
. . . 4
β’ ((
βf + βΎ (π΅ Γ π΅)) β V β ( βf
+ βΎ
(π΅ Γ π΅)) =
(+gβ({β¨(Baseβndx), π΅β©, β¨(+gβndx), (
βf + βΎ (π΅ Γ π΅))β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ (({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ
{(TopOpenβπ
)}))β©}))) |
27 | 19, 20, 26 | mp2b 10 |
. . 3
β’ (
βf + βΎ (π΅ Γ π΅)) =
(+gβ({β¨(Baseβndx), π΅β©, β¨(+gβndx), (
βf + βΎ (π΅ Γ π΅))β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β¦ (π
Ξ£g
(π₯ β {π¦ β {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} β£ π¦ βr β€ π} β¦ ((πβπ₯)(.rβπ
)(πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ (({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ {π₯}) βf
(.rβπ
)π))β©, β¨(TopSetβndx),
(βtβ({β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} Γ
{(TopOpenβπ
)}))β©})) |
28 | 16, 17, 27 | 3eqtr4g 2798 |
. 2
β’ ((πΌ β V β§ π
β V) β β = (
βf + βΎ (π΅ Γ π΅))) |
29 | | reldmpsr 21332 |
. . . . . . 7
β’ Rel dom
mPwSer |
30 | 29 | ovprc 7396 |
. . . . . 6
β’ (Β¬
(πΌ β V β§ π
β V) β (πΌ mPwSer π
) = β
) |
31 | 1, 30 | eqtrid 2785 |
. . . . 5
β’ (Β¬
(πΌ β V β§ π
β V) β π = β
) |
32 | 31 | fveq2d 6847 |
. . . 4
β’ (Β¬
(πΌ β V β§ π
β V) β
(+gβπ) =
(+gββ
)) |
33 | 22 | str0 17066 |
. . . 4
β’ β
=
(+gββ
) |
34 | 32, 17, 33 | 3eqtr4g 2798 |
. . 3
β’ (Β¬
(πΌ β V β§ π
β V) β β =
β
) |
35 | 31 | fveq2d 6847 |
. . . . . . . 8
β’ (Β¬
(πΌ β V β§ π
β V) β
(Baseβπ) =
(Baseββ
)) |
36 | | base0 17093 |
. . . . . . . 8
β’ β
=
(Baseββ
) |
37 | 35, 7, 36 | 3eqtr4g 2798 |
. . . . . . 7
β’ (Β¬
(πΌ β V β§ π
β V) β π΅ = β
) |
38 | 37 | xpeq2d 5664 |
. . . . . 6
β’ (Β¬
(πΌ β V β§ π
β V) β (π΅ Γ π΅) = (π΅ Γ β
)) |
39 | | xp0 6111 |
. . . . . 6
β’ (π΅ Γ β
) =
β
|
40 | 38, 39 | eqtrdi 2789 |
. . . . 5
β’ (Β¬
(πΌ β V β§ π
β V) β (π΅ Γ π΅) = β
) |
41 | 40 | reseq2d 5938 |
. . . 4
β’ (Β¬
(πΌ β V β§ π
β V) β (
βf + βΎ (π΅ Γ π΅)) = ( βf + βΎ
β
)) |
42 | | res0 5942 |
. . . 4
β’ (
βf + βΎ β
) =
β
|
43 | 41, 42 | eqtrdi 2789 |
. . 3
β’ (Β¬
(πΌ β V β§ π
β V) β (
βf + βΎ (π΅ Γ π΅)) = β
) |
44 | 34, 43 | eqtr4d 2776 |
. 2
β’ (Β¬
(πΌ β V β§ π
β V) β β = (
βf + βΎ (π΅ Γ π΅))) |
45 | 28, 44 | pm2.61i 182 |
1
β’ β = (
βf + βΎ (π΅ Γ π΅)) |