Step | Hyp | Ref
| Expression |
1 | | psrvsca.s |
. . . . 5
β’ π = (πΌ mPwSer π
) |
2 | | psrvsca.k |
. . . . 5
β’ πΎ = (Baseβπ
) |
3 | | eqid 2733 |
. . . . 5
β’
(+gβπ
) = (+gβπ
) |
4 | | psrvsca.m |
. . . . 5
β’ Β· =
(.rβπ
) |
5 | | eqid 2733 |
. . . . 5
β’
(TopOpenβπ
) =
(TopOpenβπ
) |
6 | | psrvsca.d |
. . . . 5
β’ π· = {β β (β0
βm πΌ)
β£ (β‘β β β) β Fin} |
7 | | psrvsca.b |
. . . . . 6
β’ π΅ = (Baseβπ) |
8 | | simpl 484 |
. . . . . 6
β’ ((πΌ β V β§ π
β V) β πΌ β V) |
9 | 1, 2, 6, 7, 8 | psrbas 21362 |
. . . . 5
β’ ((πΌ β V β§ π
β V) β π΅ = (πΎ βm π·)) |
10 | | eqid 2733 |
. . . . . 6
β’
(+gβπ) = (+gβπ) |
11 | 1, 7, 3, 10 | psrplusg 21365 |
. . . . 5
β’
(+gβπ) = ( βf
(+gβπ
)
βΎ (π΅ Γ π΅)) |
12 | | eqid 2733 |
. . . . . 6
β’
(.rβπ) = (.rβπ) |
13 | 1, 7, 4, 12, 6 | psrmulr 21368 |
. . . . 5
β’
(.rβπ) = (π β π΅, π β π΅ β¦ (π β π· β¦ (π
Ξ£g (π₯ β {π¦ β π· β£ π¦ βr β€ π} β¦ ((πβπ₯) Β· (πβ(π βf β π₯))))))) |
14 | | eqid 2733 |
. . . . 5
β’ (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π)) = (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π)) |
15 | | eqidd 2734 |
. . . . 5
β’ ((πΌ β V β§ π
β V) β
(βtβ(π· Γ {(TopOpenβπ
)})) = (βtβ(π· Γ {(TopOpenβπ
)}))) |
16 | | simpr 486 |
. . . . 5
β’ ((πΌ β V β§ π
β V) β π
β V) |
17 | 1, 2, 3, 4, 5, 6, 9, 11, 13, 14, 15, 8, 16 | psrval 21333 |
. . . 4
β’ ((πΌ β V β§ π
β V) β π = ({β¨(Baseβndx),
π΅β©,
β¨(+gβndx), (+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©})) |
18 | 17 | fveq2d 6847 |
. . 3
β’ ((πΌ β V β§ π
β V) β (
Β·π βπ) = ( Β·π
β({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}))) |
19 | | psrvsca.n |
. . 3
β’ β = (
Β·π βπ) |
20 | 2 | fvexi 6857 |
. . . . 5
β’ πΎ β V |
21 | 7 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
22 | 20, 21 | mpoex 8013 |
. . . 4
β’ (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π)) β V |
23 | | psrvalstr 21334 |
. . . . 5
β’
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}) Struct β¨1,
9β© |
24 | | vscaid 17206 |
. . . . 5
β’
Β·π = Slot (
Β·π βndx) |
25 | | snsstp2 4778 |
. . . . . 6
β’ {β¨(
Β·π βndx), (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©} β {β¨(Scalarβndx),
π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©} |
26 | | ssun2 4134 |
. . . . . 6
β’
{β¨(Scalarβndx), π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©} β
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}) |
27 | 25, 26 | sstri 3954 |
. . . . 5
β’ {β¨(
Β·π βndx), (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©} β ({β¨(Baseβndx),
π΅β©,
β¨(+gβndx), (+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}) |
28 | 23, 24, 27 | strfv 17081 |
. . . 4
β’ ((π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π)) β V β (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π)) = ( Β·π
β({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©}))) |
29 | 22, 28 | ax-mp 5 |
. . 3
β’ (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π)) = ( Β·π
β({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
π
β©, β¨(
Β·π βndx), (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))β©, β¨(TopSetβndx),
(βtβ(π· Γ {(TopOpenβπ
)}))β©})) |
30 | 18, 19, 29 | 3eqtr4g 2798 |
. 2
β’ ((πΌ β V β§ π
β V) β β =
(π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))) |
31 | | eqid 2733 |
. . . . . 6
β’ β
=
β
|
32 | | fn0 6633 |
. . . . . 6
β’ (β
Fn β
β β
= β
) |
33 | 31, 32 | mpbir 230 |
. . . . 5
β’ β
Fn β
|
34 | | reldmpsr 21332 |
. . . . . . . . . 10
β’ Rel dom
mPwSer |
35 | 34 | ovprc 7396 |
. . . . . . . . 9
β’ (Β¬
(πΌ β V β§ π
β V) β (πΌ mPwSer π
) = β
) |
36 | 1, 35 | eqtrid 2785 |
. . . . . . . 8
β’ (Β¬
(πΌ β V β§ π
β V) β π = β
) |
37 | 36 | fveq2d 6847 |
. . . . . . 7
β’ (Β¬
(πΌ β V β§ π
β V) β (
Β·π βπ) = ( Β·π
ββ
)) |
38 | 24 | str0 17066 |
. . . . . . 7
β’ β
=
( Β·π ββ
) |
39 | 37, 19, 38 | 3eqtr4g 2798 |
. . . . . 6
β’ (Β¬
(πΌ β V β§ π
β V) β β =
β
) |
40 | 34, 1, 7 | elbasov 17095 |
. . . . . . . . . 10
β’ (π β π΅ β (πΌ β V β§ π
β V)) |
41 | 40 | con3i 154 |
. . . . . . . . 9
β’ (Β¬
(πΌ β V β§ π
β V) β Β¬ π β π΅) |
42 | 41 | eq0rdv 4365 |
. . . . . . . 8
β’ (Β¬
(πΌ β V β§ π
β V) β π΅ = β
) |
43 | 42 | xpeq2d 5664 |
. . . . . . 7
β’ (Β¬
(πΌ β V β§ π
β V) β (πΎ Γ π΅) = (πΎ Γ β
)) |
44 | | xp0 6111 |
. . . . . . 7
β’ (πΎ Γ β
) =
β
|
45 | 43, 44 | eqtrdi 2789 |
. . . . . 6
β’ (Β¬
(πΌ β V β§ π
β V) β (πΎ Γ π΅) = β
) |
46 | 39, 45 | fneq12d 6598 |
. . . . 5
β’ (Β¬
(πΌ β V β§ π
β V) β ( β Fn
(πΎ Γ π΅) β β
Fn
β
)) |
47 | 33, 46 | mpbiri 258 |
. . . 4
β’ (Β¬
(πΌ β V β§ π
β V) β β Fn
(πΎ Γ π΅)) |
48 | | fnov 7488 |
. . . 4
β’ ( β Fn
(πΎ Γ π΅) β β = (π₯ β πΎ, π β π΅ β¦ (π₯ β π))) |
49 | 47, 48 | sylib 217 |
. . 3
β’ (Β¬
(πΌ β V β§ π
β V) β β =
(π₯ β πΎ, π β π΅ β¦ (π₯ β π))) |
50 | 41 | pm2.21d 121 |
. . . . . 6
β’ (Β¬
(πΌ β V β§ π
β V) β (π β π΅ β ((π· Γ {π₯}) βf Β· π) = (π₯ β π))) |
51 | 50 | a1d 25 |
. . . . 5
β’ (Β¬
(πΌ β V β§ π
β V) β (π₯ β πΎ β (π β π΅ β ((π· Γ {π₯}) βf Β· π) = (π₯ β π)))) |
52 | 51 | 3imp 1112 |
. . . 4
β’ ((Β¬
(πΌ β V β§ π
β V) β§ π₯ β πΎ β§ π β π΅) β ((π· Γ {π₯}) βf Β· π) = (π₯ β π)) |
53 | 52 | mpoeq3dva 7435 |
. . 3
β’ (Β¬
(πΌ β V β§ π
β V) β (π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π)) = (π₯ β πΎ, π β π΅ β¦ (π₯ β π))) |
54 | 49, 53 | eqtr4d 2776 |
. 2
β’ (Β¬
(πΌ β V β§ π
β V) β β =
(π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π))) |
55 | 30, 54 | pm2.61i 182 |
1
β’ β =
(π₯ β πΎ, π β π΅ β¦ ((π· Γ {π₯}) βf Β· π)) |