Step | Hyp | Ref
| Expression |
1 | | psrval.s |
. 2
⢠ð = (ðŒ mPwSer ð
) |
2 | | df-psr 21264 |
. . . 4
⢠mPwSer =
(ð â V, ð â V âŠ
âŠ{â â
(â0 âm ð) ⣠(â¡â â â) â Fin} / ðâŠâŠ((Baseâð) âm ð) / ðâŠ({âš(Baseândx), ðâ©,
âš(+gândx), ( âf (+gâð) ⟠(ð à ð))â©, âš(.rândx),
(ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â©} ⪠{âš(Scalarândx),
ðâ©, âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â©, âš(TopSetândx),
(âtâ(ð
à {(TopOpenâð)}))â©})) |
3 | 2 | a1i 11 |
. . 3
⢠(ð â mPwSer = (ð â V, ð â V ⊠âŠ{â â (â0
âm ð)
⣠(â¡â â â) â Fin} / ðâŠâŠ((Baseâð) âm ð) / ðâŠ({âš(Baseândx), ðâ©,
âš(+gândx), ( âf (+gâð) ⟠(ð à ð))â©, âš(.rândx),
(ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â©} ⪠{âš(Scalarândx),
ðâ©, âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â©, âš(TopSetândx),
(âtâ(ð
à {(TopOpenâð)}))â©}))) |
4 | | simprl 769 |
. . . . . . . 8
⢠((ð ⧠(ð = ðŒ ⧠ð = ð
)) â ð = ðŒ) |
5 | 4 | oveq2d 7367 |
. . . . . . 7
⢠((ð ⧠(ð = ðŒ ⧠ð = ð
)) â (â0
âm ð) =
(â0 âm ðŒ)) |
6 | | rabeq 3419 |
. . . . . . 7
â¢
((â0 âm ð) = (â0 âm
ðŒ) â {â â (â0
âm ð)
⣠(â¡â â â) â Fin} = {â â (â0
âm ðŒ)
⣠(â¡â â â) â
Fin}) |
7 | 5, 6 | syl 17 |
. . . . . 6
⢠((ð ⧠(ð = ðŒ ⧠ð = ð
)) â {â â (â0
âm ð)
⣠(â¡â â â) â Fin} = {â â (â0
âm ðŒ)
⣠(â¡â â â) â
Fin}) |
8 | | psrval.d |
. . . . . 6
⢠ð· = {â â (â0
âm ðŒ)
⣠(â¡â â â) â Fin} |
9 | 7, 8 | eqtr4di 2795 |
. . . . 5
⢠((ð ⧠(ð = ðŒ ⧠ð = ð
)) â {â â (â0
âm ð)
⣠(â¡â â â) â Fin} = ð·) |
10 | 9 | csbeq1d 3857 |
. . . 4
⢠((ð ⧠(ð = ðŒ ⧠ð = ð
)) â âŠ{â â (â0
âm ð)
⣠(â¡â â â) â Fin} / ðâŠâŠ((Baseâð) âm ð) / ðâŠ({âš(Baseândx), ðâ©,
âš(+gândx), ( âf (+gâð) ⟠(ð à ð))â©, âš(.rândx),
(ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â©} ⪠{âš(Scalarândx),
ðâ©, âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â©, âš(TopSetândx),
(âtâ(ð
à {(TopOpenâð)}))â©}) = âŠð· / ðâŠâŠ((Baseâð) âm ð) / ðâŠ({âš(Baseândx), ðâ©,
âš(+gândx), ( âf (+gâð) ⟠(ð à ð))â©, âš(.rândx),
(ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â©} ⪠{âš(Scalarândx),
ðâ©, âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â©, âš(TopSetândx),
(âtâ(ð
à {(TopOpenâð)}))â©})) |
11 | | ovex 7384 |
. . . . . . 7
â¢
(â0 âm ð) â V |
12 | 11 | rabex 5287 |
. . . . . 6
⢠{â â (â0
âm ð)
⣠(â¡â â â) â Fin} â
V |
13 | 9, 12 | eqeltrrdi 2847 |
. . . . 5
⢠((ð ⧠(ð = ðŒ ⧠ð = ð
)) â ð· â V) |
14 | | simplrr 776 |
. . . . . . . . . . 11
⢠(((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) â ð = ð
) |
15 | 14 | fveq2d 6843 |
. . . . . . . . . 10
⢠(((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) â (Baseâð) = (Baseâð
)) |
16 | | psrval.k |
. . . . . . . . . 10
⢠ðŸ = (Baseâð
) |
17 | 15, 16 | eqtr4di 2795 |
. . . . . . . . 9
⢠(((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) â (Baseâð) = ðŸ) |
18 | | simpr 485 |
. . . . . . . . 9
⢠(((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) â ð = ð·) |
19 | 17, 18 | oveq12d 7369 |
. . . . . . . 8
⢠(((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) â ((Baseâð) âm ð) = (ðŸ âm ð·)) |
20 | | psrval.b |
. . . . . . . . 9
⢠(ð â ðµ = (ðŸ âm ð·)) |
21 | 20 | ad2antrr 724 |
. . . . . . . 8
⢠(((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) â ðµ = (ðŸ âm ð·)) |
22 | 19, 21 | eqtr4d 2780 |
. . . . . . 7
⢠(((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) â ((Baseâð) âm ð) = ðµ) |
23 | 22 | csbeq1d 3857 |
. . . . . 6
⢠(((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) â âŠ((Baseâð) âm ð) / ðâŠ({âš(Baseândx),
ðâ©,
âš(+gândx), ( âf
(+gâð)
⟠(ð à ð))â©,
âš(.rândx), (ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â©} âª
{âš(Scalarândx), ðâ©, âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â©, âš(TopSetândx),
(âtâ(ð à {(TopOpenâð)}))â©}) = âŠðµ / ðâŠ({âš(Baseândx),
ðâ©,
âš(+gândx), ( âf
(+gâð)
⟠(ð à ð))â©,
âš(.rândx), (ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â©} âª
{âš(Scalarândx), ðâ©, âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â©, âš(TopSetândx),
(âtâ(ð Ã {(TopOpenâð)}))â©})) |
24 | | ovex 7384 |
. . . . . . . 8
â¢
((Baseâð)
âm ð)
â V |
25 | 22, 24 | eqeltrrdi 2847 |
. . . . . . 7
⢠(((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) â ðµ â V) |
26 | | simpr 485 |
. . . . . . . . . 10
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â ð = ðµ) |
27 | 26 | opeq2d 4835 |
. . . . . . . . 9
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â âš(Baseândx), ðâ© = âš(Baseândx),
ðµâ©) |
28 | 14 | adantr 481 |
. . . . . . . . . . . . . . 15
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â ð = ð
) |
29 | 28 | fveq2d 6843 |
. . . . . . . . . . . . . 14
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (+gâð) = (+gâð
)) |
30 | | psrval.a |
. . . . . . . . . . . . . 14
⢠+ =
(+gâð
) |
31 | 29, 30 | eqtr4di 2795 |
. . . . . . . . . . . . 13
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (+gâð) = + ) |
32 | 31 | ofeqd 7611 |
. . . . . . . . . . . 12
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â âf
(+gâð) =
âf + ) |
33 | 26, 26 | xpeq12d 5662 |
. . . . . . . . . . . 12
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (ð à ð) = (ðµ à ðµ)) |
34 | 32, 33 | reseq12d 5936 |
. . . . . . . . . . 11
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â ( âf
(+gâð)
⟠(ð à ð)) = ( âf + âŸ
(ðµ Ã ðµ))) |
35 | | psrval.p |
. . . . . . . . . . 11
⢠â = (
âf + ⟠(ðµ à ðµ)) |
36 | 34, 35 | eqtr4di 2795 |
. . . . . . . . . 10
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â ( âf
(+gâð)
⟠(ð à ð)) = â ) |
37 | 36 | opeq2d 4835 |
. . . . . . . . 9
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â âš(+gândx), (
âf (+gâð) ⟠(ð à ð))â© = âš(+gândx),
â
â©) |
38 | 18 | adantr 481 |
. . . . . . . . . . . . 13
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â ð = ð·) |
39 | | rabeq 3419 |
. . . . . . . . . . . . . . . 16
⢠(ð = ð· â {ðŠ â ð ⣠ðŠ âr †ð} = {ðŠ â ð· ⣠ðŠ âr †ð}) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . . 15
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â {ðŠ â ð ⣠ðŠ âr †ð} = {ðŠ â ð· ⣠ðŠ âr †ð}) |
41 | 28 | fveq2d 6843 |
. . . . . . . . . . . . . . . . 17
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (.râð) = (.râð
)) |
42 | | psrval.m |
. . . . . . . . . . . . . . . . 17
⢠· =
(.râð
) |
43 | 41, 42 | eqtr4di 2795 |
. . . . . . . . . . . . . . . 16
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (.râð) = · ) |
44 | 43 | oveqd 7368 |
. . . . . . . . . . . . . . 15
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â ((ðâð¥)(.râð)(ðâ(ð âf â ð¥))) = ((ðâð¥) · (ðâ(ð âf â ð¥)))) |
45 | 40, 44 | mpteq12dv 5194 |
. . . . . . . . . . . . . 14
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))) = (ð¥ â {ðŠ â ð· ⣠ðŠ âr †ð} ⊠((ðâð¥) · (ðâ(ð âf â ð¥))))) |
46 | 28, 45 | oveq12d 7369 |
. . . . . . . . . . . . 13
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥))))) = (ð
Σg (ð¥ â {ðŠ â ð· ⣠ðŠ âr †ð} ⊠((ðâð¥) · (ðâ(ð âf â ð¥)))))) |
47 | 38, 46 | mpteq12dv 5194 |
. . . . . . . . . . . 12
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))) = (ð â ð· ⊠(ð
Σg (ð¥ â {ðŠ â ð· ⣠ðŠ âr †ð} ⊠((ðâð¥) · (ðâ(ð âf â ð¥))))))) |
48 | 26, 26, 47 | mpoeq123dv 7426 |
. . . . . . . . . . 11
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥))))))) = (ð â ðµ, ð â ðµ ⊠(ð â ð· ⊠(ð
Σg (ð¥ â {ðŠ â ð· ⣠ðŠ âr †ð} ⊠((ðâð¥) · (ðâ(ð âf â ð¥)))))))) |
49 | | psrval.t |
. . . . . . . . . . 11
⢠à =
(ð â ðµ, ð â ðµ ⊠(ð â ð· ⊠(ð
Σg (ð¥ â {ðŠ â ð· ⣠ðŠ âr †ð} ⊠((ðâð¥) · (ðâ(ð âf â ð¥))))))) |
50 | 48, 49 | eqtr4di 2795 |
. . . . . . . . . 10
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥))))))) = à ) |
51 | 50 | opeq2d 4835 |
. . . . . . . . 9
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â âš(.rândx),
(ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â© =
âš(.rândx), Ã
â©) |
52 | 27, 37, 51 | tpeq123d 4707 |
. . . . . . . 8
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â {âš(Baseândx), ðâ©,
âš(+gândx), ( âf
(+gâð)
⟠(ð à ð))â©,
âš(.rândx), (ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â©} =
{âš(Baseândx), ðµâ©, âš(+gândx),
â
â©, âš(.rândx), Ã
â©}) |
53 | 28 | opeq2d 4835 |
. . . . . . . . 9
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â âš(Scalarândx), ðâ© =
âš(Scalarândx), ð
â©) |
54 | 17 | adantr 481 |
. . . . . . . . . . . 12
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (Baseâð) = ðŸ) |
55 | 43 | ofeqd 7611 |
. . . . . . . . . . . . 13
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â âf
(.râð) =
âf · ) |
56 | 38 | xpeq1d 5660 |
. . . . . . . . . . . . 13
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (ð à {ð¥}) = (ð· à {ð¥})) |
57 | | eqidd 2738 |
. . . . . . . . . . . . 13
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â ð = ð) |
58 | 55, 56, 57 | oveq123d 7372 |
. . . . . . . . . . . 12
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â ((ð à {ð¥}) âf
(.râð)ð) = ((ð· à {ð¥}) âf · ð)) |
59 | 54, 26, 58 | mpoeq123dv 7426 |
. . . . . . . . . . 11
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð)) = (ð¥ â ðŸ, ð â ðµ ⊠((ð· à {ð¥}) âf · ð))) |
60 | | psrval.v |
. . . . . . . . . . 11
⢠â =
(ð¥ â ðŸ, ð â ðµ ⊠((ð· à {ð¥}) âf · ð)) |
61 | 59, 60 | eqtr4di 2795 |
. . . . . . . . . 10
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð)) = â ) |
62 | 61 | opeq2d 4835 |
. . . . . . . . 9
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â© = âš(
·ð ândx), â
â©) |
63 | 28 | fveq2d 6843 |
. . . . . . . . . . . . . . 15
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (TopOpenâð) = (TopOpenâð
)) |
64 | | psrval.o |
. . . . . . . . . . . . . . 15
⢠ð = (TopOpenâð
) |
65 | 63, 64 | eqtr4di 2795 |
. . . . . . . . . . . . . 14
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (TopOpenâð) = ð) |
66 | 65 | sneqd 4596 |
. . . . . . . . . . . . 13
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â {(TopOpenâð)} = {ð}) |
67 | 38, 66 | xpeq12d 5662 |
. . . . . . . . . . . 12
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (ð à {(TopOpenâð)}) = (ð· à {ð})) |
68 | 67 | fveq2d 6843 |
. . . . . . . . . . 11
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (âtâ(ð à {(TopOpenâð)})) =
(âtâ(ð· Ã {ð}))) |
69 | | psrval.j |
. . . . . . . . . . . 12
⢠(ð â ðœ = (âtâ(ð· à {ð}))) |
70 | 69 | ad3antrrr 728 |
. . . . . . . . . . 11
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â ðœ = (âtâ(ð· à {ð}))) |
71 | 68, 70 | eqtr4d 2780 |
. . . . . . . . . 10
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â (âtâ(ð à {(TopOpenâð)})) = ðœ) |
72 | 71 | opeq2d 4835 |
. . . . . . . . 9
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â âš(TopSetândx),
(âtâ(ð à {(TopOpenâð)}))â© = âš(TopSetândx), ðœâ©) |
73 | 53, 62, 72 | tpeq123d 4707 |
. . . . . . . 8
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â {âš(Scalarândx), ðâ©, âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â©, âš(TopSetândx),
(âtâ(ð Ã {(TopOpenâð)}))â©} = {âš(Scalarândx),
ð
â©, âš(
·ð ândx), â â©,
âš(TopSetândx), ðœâ©}) |
74 | 52, 73 | uneq12d 4122 |
. . . . . . 7
⢠((((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) ⧠ð = ðµ) â ({âš(Baseândx), ðâ©,
âš(+gândx), ( âf
(+gâð)
⟠(ð à ð))â©,
âš(.rândx), (ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â©} âª
{âš(Scalarândx), ðâ©, âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â©, âš(TopSetândx),
(âtâ(ð Ã {(TopOpenâð)}))â©}) = ({âš(Baseândx),
ðµâ©,
âš(+gândx), â â©,
âš(.rândx), à â©} âª
{âš(Scalarândx), ð
â©, âš(
·ð ândx), â â©,
âš(TopSetândx), ðœâ©})) |
75 | 25, 74 | csbied 3891 |
. . . . . 6
⢠(((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) â âŠðµ / ðâŠ({âš(Baseândx),
ðâ©,
âš(+gândx), ( âf
(+gâð)
⟠(ð à ð))â©,
âš(.rândx), (ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â©} âª
{âš(Scalarândx), ðâ©, âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â©, âš(TopSetândx),
(âtâ(ð Ã {(TopOpenâð)}))â©}) = ({âš(Baseândx),
ðµâ©,
âš(+gândx), â â©,
âš(.rândx), à â©} âª
{âš(Scalarândx), ð
â©, âš(
·ð ândx), â â©,
âš(TopSetândx), ðœâ©})) |
76 | 23, 75 | eqtrd 2777 |
. . . . 5
⢠(((ð ⧠(ð = ðŒ ⧠ð = ð
)) ⧠ð = ð·) â âŠ((Baseâð) âm ð) / ðâŠ({âš(Baseândx),
ðâ©,
âš(+gândx), ( âf
(+gâð)
⟠(ð à ð))â©,
âš(.rândx), (ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â©} âª
{âš(Scalarândx), ðâ©, âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â©, âš(TopSetândx),
(âtâ(ð Ã {(TopOpenâð)}))â©}) = ({âš(Baseândx),
ðµâ©,
âš(+gândx), â â©,
âš(.rândx), à â©} âª
{âš(Scalarândx), ð
â©, âš(
·ð ândx), â â©,
âš(TopSetândx), ðœâ©})) |
77 | 13, 76 | csbied 3891 |
. . . 4
⢠((ð ⧠(ð = ðŒ ⧠ð = ð
)) â âŠð· / ðâŠâŠ((Baseâð) âm ð) / ðâŠ({âš(Baseândx), ðâ©,
âš(+gândx), ( âf (+gâð) ⟠(ð à ð))â©, âš(.rândx),
(ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â©} ⪠{âš(Scalarândx),
ðâ©, âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â©, âš(TopSetândx),
(âtâ(ð
à {(TopOpenâð)}))â©}) = ({âš(Baseândx), ðµâ©,
âš(+gândx), â â©,
âš(.rândx), à â©} âª
{âš(Scalarândx), ð
â©, âš(
·ð ândx), â â©,
âš(TopSetândx), ðœâ©})) |
78 | 10, 77 | eqtrd 2777 |
. . 3
⢠((ð ⧠(ð = ðŒ ⧠ð = ð
)) â âŠ{â â (â0
âm ð)
⣠(â¡â â â) â Fin} / ðâŠâŠ((Baseâð) âm ð) / ðâŠ({âš(Baseândx), ðâ©,
âš(+gândx), ( âf (+gâð) ⟠(ð à ð))â©, âš(.rândx),
(ð â ð, ð â ð ⊠(ð â ð ⊠(ð Σg (ð¥ â {ðŠ â ð ⣠ðŠ âr †ð} ⊠((ðâð¥)(.râð)(ðâ(ð âf â ð¥)))))))â©} ⪠{âš(Scalarândx),
ðâ©, âš(
·ð ândx), (ð¥ â (Baseâð), ð â ð ⊠((ð à {ð¥}) âf
(.râð)ð))â©, âš(TopSetândx),
(âtâ(ð
à {(TopOpenâð)}))â©}) = ({âš(Baseândx), ðµâ©,
âš(+gândx), â â©,
âš(.rândx), à â©} âª
{âš(Scalarândx), ð
â©, âš(
·ð ândx), â â©,
âš(TopSetândx), ðœâ©})) |
79 | | psrval.i |
. . . 4
⢠(ð â ðŒ â ð) |
80 | 79 | elexd 3463 |
. . 3
⢠(ð â ðŒ â V) |
81 | | psrval.r |
. . . 4
⢠(ð â ð
â ð) |
82 | 81 | elexd 3463 |
. . 3
⢠(ð â ð
â V) |
83 | | tpex 7673 |
. . . . 5
â¢
{âš(Baseândx), ðµâ©, âš(+gândx),
â
â©, âš(.rândx), Ã â©} â
V |
84 | | tpex 7673 |
. . . . 5
â¢
{âš(Scalarândx), ð
â©, âš(
·ð ândx), â â©,
âš(TopSetândx), ðœâ©} â V |
85 | 83, 84 | unex 7672 |
. . . 4
â¢
({âš(Baseândx), ðµâ©, âš(+gândx),
â
â©, âš(.rândx), à â©} âª
{âš(Scalarândx), ð
â©, âš(
·ð ândx), â â©,
âš(TopSetândx), ðœâ©}) â V |
86 | 85 | a1i 11 |
. . 3
⢠(ð â ({âš(Baseândx),
ðµâ©,
âš(+gândx), â â©,
âš(.rândx), à â©} âª
{âš(Scalarândx), ð
â©, âš(
·ð ândx), â â©,
âš(TopSetândx), ðœâ©}) â V) |
87 | 3, 78, 80, 82, 86 | ovmpod 7501 |
. 2
⢠(ð â (ðŒ mPwSer ð
) = ({âš(Baseândx), ðµâ©,
âš(+gândx), â â©,
âš(.rândx), à â©} âª
{âš(Scalarândx), ð
â©, âš(
·ð ândx), â â©,
âš(TopSetândx), ðœâ©})) |
88 | 1, 87 | eqtrid 2789 |
1
⢠(ð â ð = ({âš(Baseândx), ðµâ©,
âš(+gândx), â â©,
âš(.rândx), à â©} âª
{âš(Scalarândx), ð
â©, âš(
·ð ândx), â â©,
âš(TopSetândx), ðœâ©})) |