Step | Hyp | Ref
| Expression |
1 | | psrmulr.s |
. . . . 5
β’ π = (πΌ mPwSer π
) |
2 | | eqid 2733 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
3 | | eqid 2733 |
. . . . 5
β’
(+gβπ
) = (+gβπ
) |
4 | | psrmulr.m |
. . . . 5
β’ Β· =
(.rβπ
) |
5 | | eqid 2733 |
. . . . 5
β’
(TopOpenβπ
) =
(TopOpenβπ
) |
6 | | psrmulr.d |
. . . . 5
β’ π· = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
7 | | psrmulr.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
8 | | simpl 484 |
. . . . . 6
β’ ((πΌ β V β§ π
β V) β πΌ β V) |
9 | 1, 2, 6, 7, 8 | psrbas 21362 |
. . . . 5
β’ ((πΌ β V β§ π
β V) β π΅ = ((Baseβπ
) βm π·)) |
10 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
11 | 1, 7, 3, 10 | psrplusg 21365 |
. . . . 5
β’
(+gβπ) = ( βf
(+gβπ
)
βΎ (π΅ Γ π΅)) |
12 | | eqid 2733 |
. . . . 5
β’ (π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯))))))) = (π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯))))))) |
13 | | eqid 2733 |
. . . . 5
β’ (π₯ β (Baseβπ
), π β π΅ β¦ ((π· Γ {π₯}) βf Β· π)) = (π₯ β (Baseβπ
), π β π΅ β¦ ((π· Γ {π₯}) βf Β· π)) |
14 | | eqidd 2734 |
. . . . 5
β’ ((πΌ β V β§ π
β V) β
(βtβ(π· Γ {(TopOpenβπ
)})) = (βtβ(π· Γ {(TopOpenβπ
)}))) |
15 | | simpr 486 |
. . . . 5
β’ ((πΌ β V β§ π
β V) β π
β V) |
16 | 1, 2, 3, 4, 5, 6, 9, 11, 12, 13, 14, 8, 15 | psrval 21333 |
. . . 4
β’ ((πΌ β V β§ π
β V) β π = ({β¨(Baseβndx),
π΅β©,
β¨(+gβndx), (+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©})) |
17 | 16 | fveq2d 6847 |
. . 3
β’ ((πΌ β V β§ π
β V) β
(.rβπ) =
(.rβ({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}))) |
18 | | psrmulr.t |
. . 3
β’ β =
(.rβπ) |
19 | 7 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
20 | 19, 19 | mpoex 8013 |
. . . 4
β’ (π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯))))))) β
V |
21 | | psrvalstr 21334 |
. . . . 5
β’
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}) Struct β¨1,
9β© |
22 | | mulrid 17180 |
. . . . 5
β’
.r = Slot (.rβndx) |
23 | | snsstp3 4779 |
. . . . . 6
β’
{β¨(.rβndx), (π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))β©} β
{β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))β©} |
24 | | ssun1 4133 |
. . . . . 6
β’
{β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))β©} β
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}) |
25 | 23, 24 | sstri 3954 |
. . . . 5
β’
{β¨(.rβndx), (π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))β©} β
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}) |
26 | 21, 22, 25 | strfv 17081 |
. . . 4
β’ ((π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯))))))) β V β (π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯))))))) =
(.rβ({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}))) |
27 | 20, 26 | ax-mp 5 |
. . 3
β’ (π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯))))))) =
(.rβ({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))β©} βͺ
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β (Baseβπ
), π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©})) |
28 | 17, 18, 27 | 3eqtr4g 2798 |
. 2
β’ ((πΌ β V β§ π
β V) β β =
(π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))) |
29 | 22 | str0 17066 |
. . . 4
β’ β
=
(.rββ
) |
30 | 29 | eqcomi 2742 |
. . 3
β’
(.rββ
) = β
|
31 | | reldmpsr 21332 |
. . . . . . 7
β’ Rel dom
mPwSer |
32 | 31 | ovprc 7396 |
. . . . . 6
β’ (Β¬
(πΌ β V β§ π
β V) β (πΌ mPwSer π
) = β
) |
33 | 1, 32 | eqtrid 2785 |
. . . . 5
β’ (Β¬
(πΌ β V β§ π
β V) β π = β
) |
34 | 33 | fveq2d 6847 |
. . . 4
β’ (Β¬
(πΌ β V β§ π
β V) β
(.rβπ) =
(.rββ
)) |
35 | 18, 34 | eqtrid 2785 |
. . 3
β’ (Β¬
(πΌ β V β§ π
β V) β β =
(.rββ
)) |
36 | 33 | fveq2d 6847 |
. . . . . 6
β’ (Β¬
(πΌ β V β§ π
β V) β
(Baseβπ) =
(Baseββ
)) |
37 | | base0 17093 |
. . . . . 6
β’ β
=
(Baseββ
) |
38 | 36, 7, 37 | 3eqtr4g 2798 |
. . . . 5
β’ (Β¬
(πΌ β V β§ π
β V) β π΅ = β
) |
39 | 38 | olcd 873 |
. . . 4
β’ (Β¬
(πΌ β V β§ π
β V) β (π΅ = β
β¨ π΅ = β
)) |
40 | | 0mpo0 7441 |
. . . 4
β’ ((π΅ = β
β¨ π΅ = β
) β (π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯))))))) =
β
) |
41 | 39, 40 | syl 17 |
. . 3
β’ (Β¬
(πΌ β V β§ π
β V) β (π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯))))))) =
β
) |
42 | 30, 35, 41 | 3eqtr4a 2799 |
. 2
β’ (Β¬
(πΌ β V β§ π
β V) β β =
(π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯)))))))) |
43 | 28, 42 | pm2.61i 182 |
1
β’ β =
(π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯))))))) |