Step | Hyp | Ref
| Expression |
1 | | prdsbas.p |
. . 3
β’ π = (πXsπ
) |
2 | | eqid 2733 |
. . 3
β’
(Baseβπ) =
(Baseβπ) |
3 | | prdsbas.i |
. . 3
β’ (π β dom π
= πΌ) |
4 | | prdsbas.s |
. . . 4
β’ (π β π β π) |
5 | | prdsbas.r |
. . . 4
β’ (π β π
β π) |
6 | | prdsbas.b |
. . . 4
β’ π΅ = (Baseβπ) |
7 | 1, 4, 5, 6, 3 | prdsbas 17344 |
. . 3
β’ (π β π΅ = Xπ₯ β πΌ (Baseβ(π
βπ₯))) |
8 | | eqid 2733 |
. . . 4
β’
(+gβπ) = (+gβπ) |
9 | 1, 4, 5, 6, 3, 8 | prdsplusg 17345 |
. . 3
β’ (π β (+gβπ) = (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(+gβ(π
βπ₯))(πβπ₯))))) |
10 | | eqidd 2734 |
. . 3
β’ (π β (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)))) = (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))) |
11 | | eqidd 2734 |
. . 3
β’ (π β (π β (Baseβπ), π β π΅ β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯)))) = (π β (Baseβπ), π β π΅ β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))) |
12 | | eqidd 2734 |
. . 3
β’ (π β (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯))))) = (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))) |
13 | | eqidd 2734 |
. . 3
β’ (π β
(βtβ(TopOpen β π
)) = (βtβ(TopOpen
β π
))) |
14 | | eqidd 2734 |
. . 3
β’ (π β {β¨π, πβ© β£ ({π, π} β π΅ β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))} = {β¨π, πβ© β£ ({π, π} β π΅ β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))}) |
15 | | eqidd 2734 |
. . 3
β’ (π β (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, < ))
= (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))) |
16 | | eqidd 2734 |
. . 3
β’ (π β (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯))) = (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))) |
17 | | eqidd 2734 |
. . 3
β’ (π β (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯))))) = (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))) |
18 | 1, 2, 3, 7, 9, 10,
11, 12, 13, 14, 15, 16, 17, 4, 5 | prdsval 17342 |
. 2
β’ (π β π = (({β¨(Baseβndx), π΅β©,
β¨(+gβndx), (+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π β (Baseβπ), π β π΅ β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(βtβ(TopOpen β π
))β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π΅ β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))}β©, β¨(distβndx), (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©}))) |
19 | | prdsmulr.t |
. 2
β’ Β· =
(.rβπ) |
20 | | mulrid 17180 |
. 2
β’
.r = Slot (.rβndx) |
21 | | ovssunirn 7394 |
. . . . . . . . . . 11
β’ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)) β βͺ ran
(.rβ(π
βπ₯)) |
22 | 20 | strfvss 17064 |
. . . . . . . . . . . . 13
β’
(.rβ(π
βπ₯)) β βͺ ran
(π
βπ₯) |
23 | | fvssunirn 6876 |
. . . . . . . . . . . . . 14
β’ (π
βπ₯) β βͺ ran
π
|
24 | | rnss 5895 |
. . . . . . . . . . . . . 14
β’ ((π
βπ₯) β βͺ ran
π
β ran (π
βπ₯) β ran βͺ
ran π
) |
25 | | uniss 4874 |
. . . . . . . . . . . . . 14
β’ (ran
(π
βπ₯) β ran βͺ
ran π
β βͺ ran (π
βπ₯) β βͺ ran
βͺ ran π
) |
26 | 23, 24, 25 | mp2b 10 |
. . . . . . . . . . . . 13
β’ βͺ ran (π
βπ₯) β βͺ ran
βͺ ran π
|
27 | 22, 26 | sstri 3954 |
. . . . . . . . . . . 12
β’
(.rβ(π
βπ₯)) β βͺ ran
βͺ ran π
|
28 | | rnss 5895 |
. . . . . . . . . . . 12
β’
((.rβ(π
βπ₯)) β βͺ ran
βͺ ran π
β ran (.rβ(π
βπ₯)) β ran βͺ
ran βͺ ran π
) |
29 | | uniss 4874 |
. . . . . . . . . . . 12
β’ (ran
(.rβ(π
βπ₯)) β ran βͺ
ran βͺ ran π
β βͺ ran
(.rβ(π
βπ₯)) β βͺ ran
βͺ ran βͺ ran π
) |
30 | 27, 28, 29 | mp2b 10 |
. . . . . . . . . . 11
β’ βͺ ran (.rβ(π
βπ₯)) β βͺ ran
βͺ ran βͺ ran π
|
31 | 21, 30 | sstri 3954 |
. . . . . . . . . 10
β’ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)) β βͺ ran
βͺ ran βͺ ran π
|
32 | | ovex 7391 |
. . . . . . . . . . 11
β’ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)) β V |
33 | 32 | elpw 4565 |
. . . . . . . . . 10
β’ (((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)) β π« βͺ ran βͺ ran βͺ ran π
β ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)) β βͺ ran
βͺ ran βͺ ran π
) |
34 | 31, 33 | mpbir 230 |
. . . . . . . . 9
β’ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)) β π« βͺ ran βͺ ran βͺ ran π
|
35 | 34 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β πΌ) β ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)) β π« βͺ ran βͺ ran βͺ ran π
) |
36 | 35 | fmpttd 7064 |
. . . . . . 7
β’ (π β (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))):πΌβΆπ« βͺ ran βͺ ran βͺ ran π
) |
37 | | rnexg 7842 |
. . . . . . . . . . . 12
β’ (π
β π β ran π
β V) |
38 | | uniexg 7678 |
. . . . . . . . . . . 12
β’ (ran
π
β V β βͺ ran π
β V) |
39 | 5, 37, 38 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β βͺ ran π
β V) |
40 | | rnexg 7842 |
. . . . . . . . . . 11
β’ (βͺ ran π
β V β ran βͺ ran π
β V) |
41 | | uniexg 7678 |
. . . . . . . . . . 11
β’ (ran
βͺ ran π
β V β βͺ ran βͺ ran π
β V) |
42 | 39, 40, 41 | 3syl 18 |
. . . . . . . . . 10
β’ (π β βͺ ran βͺ ran π
β V) |
43 | | rnexg 7842 |
. . . . . . . . . 10
β’ (βͺ ran βͺ ran π
β V β ran βͺ ran βͺ ran π
β V) |
44 | | uniexg 7678 |
. . . . . . . . . 10
β’ (ran
βͺ ran βͺ ran π
β V β βͺ ran βͺ ran βͺ ran π
β V) |
45 | 42, 43, 44 | 3syl 18 |
. . . . . . . . 9
β’ (π β βͺ ran βͺ ran βͺ ran π
β V) |
46 | 45 | pwexd 5335 |
. . . . . . . 8
β’ (π β π« βͺ ran βͺ ran βͺ ran π
β V) |
47 | 5 | dmexd 7843 |
. . . . . . . . 9
β’ (π β dom π
β V) |
48 | 3, 47 | eqeltrrd 2835 |
. . . . . . . 8
β’ (π β πΌ β V) |
49 | 46, 48 | elmapd 8782 |
. . . . . . 7
β’ (π β ((π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))) β (π« βͺ ran βͺ ran βͺ ran π
βm πΌ) β (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))):πΌβΆπ« βͺ ran βͺ ran βͺ ran π
)) |
50 | 36, 49 | mpbird 257 |
. . . . . 6
β’ (π β (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))) β (π« βͺ ran βͺ ran βͺ ran π
βm πΌ)) |
51 | 50 | ralrimivw 3144 |
. . . . 5
β’ (π β βπ β π΅ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))) β (π« βͺ ran βͺ ran βͺ ran π
βm πΌ)) |
52 | 51 | ralrimivw 3144 |
. . . 4
β’ (π β βπ β π΅ βπ β π΅ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))) β (π« βͺ ran βͺ ran βͺ ran π
βm πΌ)) |
53 | | eqid 2733 |
. . . . 5
β’ (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)))) = (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)))) |
54 | 53 | fmpo 8001 |
. . . 4
β’
(βπ β
π΅ βπ β π΅ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))) β (π« βͺ ran βͺ ran βͺ ran π
βm πΌ) β (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)))):(π΅ Γ π΅)βΆ(π« βͺ ran βͺ ran βͺ ran π
βm πΌ)) |
55 | 52, 54 | sylib 217 |
. . 3
β’ (π β (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)))):(π΅ Γ π΅)βΆ(π« βͺ ran βͺ ran βͺ ran π
βm πΌ)) |
56 | 6 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
57 | 56, 56 | xpex 7688 |
. . . 4
β’ (π΅ Γ π΅) β V |
58 | | ovex 7391 |
. . . 4
β’
(π« βͺ ran βͺ
ran βͺ ran π
βm πΌ) β V |
59 | | fex2 7871 |
. . . 4
β’ (((π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)))):(π΅ Γ π΅)βΆ(π« βͺ ran βͺ ran βͺ ran π
βm πΌ) β§ (π΅ Γ π΅) β V β§ (π« βͺ ran βͺ ran βͺ ran π
βm πΌ) β V) β (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)))) β V) |
60 | 57, 58, 59 | mp3an23 1454 |
. . 3
β’ ((π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)))):(π΅ Γ π΅)βΆ(π« βͺ ran βͺ ran βͺ ran π
βm πΌ) β (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)))) β V) |
61 | 55, 60 | syl 17 |
. 2
β’ (π β (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯)))) β V) |
62 | | snsstp3 4779 |
. . . 4
β’
{β¨(.rβndx), (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} β {β¨(Baseβndx),
π΅β©,
β¨(+gβndx), (+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} |
63 | | ssun1 4133 |
. . . 4
β’
{β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} β ({β¨(Baseβndx),
π΅β©,
β¨(+gβndx), (+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π β (Baseβπ), π β π΅ β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) |
64 | 62, 63 | sstri 3954 |
. . 3
β’
{β¨(.rβndx), (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} β ({β¨(Baseβndx),
π΅β©,
β¨(+gβndx), (+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π β (Baseβπ), π β π΅ β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) |
65 | | ssun1 4133 |
. . 3
β’
({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π β (Baseβπ), π β π΅ β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) β (({β¨(Baseβndx),
π΅β©,
β¨(+gβndx), (+gβπ)β©, β¨(.rβndx), (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx), πβ©, β¨(
Β·π βndx), (π β (Baseβπ), π β π΅ β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(βtβ(TopOpen β π
))β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π΅ β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))}β©, β¨(distβndx), (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©})) |
66 | 64, 65 | sstri 3954 |
. 2
β’
{β¨(.rβndx), (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} β
(({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (π β (Baseβπ), π β π΅ β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))β©,
β¨(Β·πβndx), (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(βtβ(TopOpen β π
))β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π΅ β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))}β©, β¨(distβndx), (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))β©} βͺ {β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©})) |
67 | 18, 19, 20, 61, 66 | prdsbaslem 17340 |
1
β’ (π β Β· = (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))) |