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 | | eqid 2733 |
. . . 4
β’
(.rβπ) = (.rβπ) |
11 | 1, 4, 5, 6, 3, 10 | prdsmulr 17346 |
. . 3
β’ (π β (.rβπ) = (π β π΅, π β π΅ β¦ (π₯ β πΌ β¦ ((πβπ₯)(.rβ(π
βπ₯))(πβπ₯))))) |
12 | | eqid 2733 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
13 | 1, 4, 5, 6, 3, 2, 12 | prdsvsca 17347 |
. . 3
β’ (π β (
Β·π βπ) = (π β (Baseβπ), π β π΅ β¦ (π₯ β πΌ β¦ (π( Β·π
β(π
βπ₯))(πβπ₯))))) |
14 | | eqidd 2734 |
. . 3
β’ (π β (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯))))) = (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))) |
15 | | eqid 2733 |
. . . 4
β’
(TopSetβπ) =
(TopSetβπ) |
16 | 1, 4, 5, 6, 3, 15 | prdstset 17353 |
. . 3
β’ (π β (TopSetβπ) =
(βtβ(TopOpen β π
))) |
17 | | eqid 2733 |
. . . 4
β’
(leβπ) =
(leβπ) |
18 | 1, 4, 5, 6, 3, 17 | prdsle 17349 |
. . 3
β’ (π β (leβπ) = {β¨π, πβ© β£ ({π, π} β π΅ β§ βπ₯ β πΌ (πβπ₯)(leβ(π
βπ₯))(πβπ₯))}) |
19 | | eqid 2733 |
. . . 4
β’
(distβπ) =
(distβπ) |
20 | 1, 4, 5, 6, 3, 19 | prdsds 17351 |
. . 3
β’ (π β (distβπ) = (π β π΅, π β π΅ β¦ sup((ran (π₯ β πΌ β¦ ((πβπ₯)(distβ(π
βπ₯))(πβπ₯))) βͺ {0}), β*, <
))) |
21 | | eqidd 2734 |
. . 3
β’ (π β (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯))) = (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))) |
22 | | eqidd 2734 |
. . 3
β’ (π β (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯))))) = (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))) |
23 | 1, 2, 3, 7, 9, 11,
13, 14, 16, 18, 20, 21, 22, 4, 5 | prdsval 17342 |
. 2
β’ (π β π = (({β¨(Baseβndx), π΅β©,
β¨(+gβndx), (+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (
Β·π βπ)β©,
β¨(Β·πβndx), (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(TopSetβπ)β©,
β¨(leβndx), (leβπ)β©, β¨(distβndx),
(distβπ)β©} βͺ
{β¨(Hom βndx), (π
β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©}))) |
24 | | prdshom.h |
. 2
β’ π» = (Hom βπ) |
25 | | homid 17298 |
. 2
β’ Hom =
Slot (Hom βndx) |
26 | | ovssunirn 7394 |
. . . . . . . . . . 11
β’ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β βͺ ran
(Hom β(π
βπ₯)) |
27 | 25 | strfvss 17064 |
. . . . . . . . . . . . 13
β’ (Hom
β(π
βπ₯)) β βͺ ran (π
βπ₯) |
28 | | fvssunirn 6876 |
. . . . . . . . . . . . . 14
β’ (π
βπ₯) β βͺ ran
π
|
29 | | rnss 5895 |
. . . . . . . . . . . . . 14
β’ ((π
βπ₯) β βͺ ran
π
β ran (π
βπ₯) β ran βͺ
ran π
) |
30 | | uniss 4874 |
. . . . . . . . . . . . . 14
β’ (ran
(π
βπ₯) β ran βͺ
ran π
β βͺ ran (π
βπ₯) β βͺ ran
βͺ ran π
) |
31 | 28, 29, 30 | mp2b 10 |
. . . . . . . . . . . . 13
β’ βͺ ran (π
βπ₯) β βͺ ran
βͺ ran π
|
32 | 27, 31 | sstri 3954 |
. . . . . . . . . . . 12
β’ (Hom
β(π
βπ₯)) β βͺ ran βͺ ran π
|
33 | | rnss 5895 |
. . . . . . . . . . . 12
β’ ((Hom
β(π
βπ₯)) β βͺ ran βͺ ran π
β ran (Hom β(π
βπ₯)) β ran βͺ
ran βͺ ran π
) |
34 | | uniss 4874 |
. . . . . . . . . . . 12
β’ (ran (Hom
β(π
βπ₯)) β ran βͺ ran βͺ ran π
β βͺ ran
(Hom β(π
βπ₯)) β βͺ ran βͺ ran βͺ ran π
) |
35 | 32, 33, 34 | mp2b 10 |
. . . . . . . . . . 11
β’ βͺ ran (Hom β(π
βπ₯)) β βͺ ran
βͺ ran βͺ ran π
|
36 | 26, 35 | sstri 3954 |
. . . . . . . . . 10
β’ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β βͺ ran
βͺ ran βͺ ran π
|
37 | 36 | rgenw 3065 |
. . . . . . . . 9
β’
βπ₯ β
πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β βͺ ran
βͺ ran βͺ ran π
|
38 | | ss2ixp 8851 |
. . . . . . . . 9
β’
(βπ₯ β
πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β βͺ ran
βͺ ran βͺ ran π
β Xπ₯ β
πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β Xπ₯ β πΌ βͺ ran βͺ ran βͺ ran π
) |
39 | 37, 38 | ax-mp 5 |
. . . . . . . 8
β’ Xπ₯ β
πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β Xπ₯ β πΌ βͺ ran βͺ ran βͺ ran π
|
40 | 5 | dmexd 7843 |
. . . . . . . . . 10
β’ (π β dom π
β V) |
41 | 3, 40 | eqeltrrd 2835 |
. . . . . . . . 9
β’ (π β πΌ β V) |
42 | | rnexg 7842 |
. . . . . . . . . . . 12
β’ (π
β π β ran π
β V) |
43 | | uniexg 7678 |
. . . . . . . . . . . 12
β’ (ran
π
β V β βͺ ran π
β V) |
44 | 5, 42, 43 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β βͺ ran π
β V) |
45 | | rnexg 7842 |
. . . . . . . . . . 11
β’ (βͺ ran π
β V β ran βͺ ran π
β V) |
46 | | uniexg 7678 |
. . . . . . . . . . 11
β’ (ran
βͺ ran π
β V β βͺ ran βͺ ran π
β V) |
47 | 44, 45, 46 | 3syl 18 |
. . . . . . . . . 10
β’ (π β βͺ ran βͺ ran π
β V) |
48 | | rnexg 7842 |
. . . . . . . . . 10
β’ (βͺ ran βͺ ran π
β V β ran βͺ ran βͺ ran π
β V) |
49 | | uniexg 7678 |
. . . . . . . . . 10
β’ (ran
βͺ ran βͺ ran π
β V β βͺ ran βͺ ran βͺ ran π
β V) |
50 | 47, 48, 49 | 3syl 18 |
. . . . . . . . 9
β’ (π β βͺ ran βͺ ran βͺ ran π
β V) |
51 | | ixpconstg 8847 |
. . . . . . . . 9
β’ ((πΌ β V β§ βͺ ran βͺ ran βͺ ran π
β V) β Xπ₯ β
πΌ βͺ ran βͺ ran βͺ ran π
= (βͺ ran βͺ ran βͺ ran π
βm πΌ)) |
52 | 41, 50, 51 | syl2anc 585 |
. . . . . . . 8
β’ (π β Xπ₯ β
πΌ βͺ ran βͺ ran βͺ ran π
= (βͺ ran βͺ ran βͺ ran π
βm πΌ)) |
53 | 39, 52 | sseqtrid 3997 |
. . . . . . 7
β’ (π β Xπ₯ β
πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β (βͺ ran
βͺ ran βͺ ran π
βm πΌ)) |
54 | | ovex 7391 |
. . . . . . . 8
β’ (βͺ ran βͺ ran βͺ ran π
βm πΌ) β V |
55 | 54 | elpw2 5303 |
. . . . . . 7
β’ (Xπ₯ β
πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β π« (βͺ ran βͺ ran βͺ ran π
βm πΌ) β Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β (βͺ ran
βͺ ran βͺ ran π
βm πΌ)) |
56 | 53, 55 | sylibr 233 |
. . . . . 6
β’ (π β Xπ₯ β
πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β π« (βͺ ran βͺ ran βͺ ran π
βm πΌ)) |
57 | 56 | ralrimivw 3144 |
. . . . 5
β’ (π β βπ β π΅ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β π« (βͺ ran βͺ ran βͺ ran π
βm πΌ)) |
58 | 57 | ralrimivw 3144 |
. . . 4
β’ (π β βπ β π΅ βπ β π΅ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β π« (βͺ ran βͺ ran βͺ ran π
βm πΌ)) |
59 | | eqid 2733 |
. . . . 5
β’ (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯))) = (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯))) |
60 | 59 | fmpo 8001 |
. . . 4
β’
(βπ β
π΅ βπ β π΅ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)) β π« (βͺ ran βͺ ran βͺ ran π
βm πΌ) β (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯))):(π΅ Γ π΅)βΆπ« (βͺ ran βͺ ran βͺ ran π
βm πΌ)) |
61 | 58, 60 | sylib 217 |
. . 3
β’ (π β (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯))):(π΅ Γ π΅)βΆπ« (βͺ ran βͺ ran βͺ ran π
βm πΌ)) |
62 | 6 | fvexi 6857 |
. . . . 5
β’ π΅ β V |
63 | 62, 62 | xpex 7688 |
. . . 4
β’ (π΅ Γ π΅) β V |
64 | 63 | a1i 11 |
. . 3
β’ (π β (π΅ Γ π΅) β V) |
65 | 54 | pwex 5336 |
. . . 4
β’ π«
(βͺ ran βͺ ran βͺ ran π
βm πΌ) β V |
66 | 65 | a1i 11 |
. . 3
β’ (π β π« (βͺ ran βͺ ran βͺ ran π
βm πΌ) β V) |
67 | | fex2 7871 |
. . 3
β’ (((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯))):(π΅ Γ π΅)βΆπ« (βͺ ran βͺ ran βͺ ran π
βm πΌ) β§ (π΅ Γ π΅) β V β§ π« (βͺ ran βͺ ran βͺ ran π
βm πΌ) β V) β (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯))) β V) |
68 | 61, 64, 66, 67 | syl3anc 1372 |
. 2
β’ (π β (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯))) β V) |
69 | | snsspr1 4775 |
. . . 4
β’
{β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©} β {β¨(Hom βndx),
(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©} |
70 | | ssun2 4134 |
. . . 4
β’
{β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©} β
({β¨(TopSetβndx), (TopSetβπ)β©, β¨(leβndx),
(leβπ)β©,
β¨(distβndx), (distβπ)β©} βͺ {β¨(Hom βndx),
(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©}) |
71 | 69, 70 | sstri 3954 |
. . 3
β’
{β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©} β
({β¨(TopSetβndx), (TopSetβπ)β©, β¨(leβndx),
(leβπ)β©,
β¨(distβndx), (distβπ)β©} βͺ {β¨(Hom βndx),
(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©}) |
72 | | ssun2 4134 |
. . 3
β’
({β¨(TopSetβndx), (TopSetβπ)β©, β¨(leβndx),
(leβπ)β©,
β¨(distβndx), (distβπ)β©} βͺ {β¨(Hom βndx),
(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©}) β
(({β¨(Baseβndx), π΅β©, β¨(+gβndx),
(+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (
Β·π βπ)β©,
β¨(Β·πβndx), (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(TopSetβπ)β©,
β¨(leβndx), (leβπ)β©, β¨(distβndx),
(distβπ)β©} βͺ
{β¨(Hom βndx), (π
β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©})) |
73 | 71, 72 | sstri 3954 |
. 2
β’
{β¨(Hom βndx), (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©} β (({β¨(Baseβndx),
π΅β©,
β¨(+gβndx), (+gβπ)β©, β¨(.rβndx),
(.rβπ)β©} βͺ {β¨(Scalarβndx),
πβ©, β¨(
Β·π βndx), (
Β·π βπ)β©,
β¨(Β·πβndx), (π β π΅, π β π΅ β¦ (π Ξ£g (π₯ β πΌ β¦ ((πβπ₯)(Β·πβ(π
βπ₯))(πβπ₯)))))β©}) βͺ ({β¨(TopSetβndx),
(TopSetβπ)β©,
β¨(leβndx), (leβπ)β©, β¨(distβndx),
(distβπ)β©} βͺ
{β¨(Hom βndx), (π
β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))β©, β¨(compβndx), (π β (π΅ Γ π΅), π β π΅ β¦ (π β ((2nd βπ)(π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))π), π β ((π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))βπ) β¦ (π₯ β πΌ β¦ ((πβπ₯)(β¨((1st βπ)βπ₯), ((2nd βπ)βπ₯)β©(compβ(π
βπ₯))(πβπ₯))(πβπ₯)))))β©})) |
74 | 23, 24, 25, 68, 73 | prdsbaslem 17340 |
1
β’ (π β π» = (π β π΅, π β π΅ β¦ Xπ₯ β πΌ ((πβπ₯)(Hom β(π
βπ₯))(πβπ₯)))) |