Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . 5
β’
(Baseβπ
) =
(Baseβπ
) |
2 | | eqid 2733 |
. . . . 5
β’
(0gβπ
) = (0gβπ
) |
3 | | psrring.r |
. . . . . . 7
β’ (π β π
β Ring) |
4 | | ringcmn 20099 |
. . . . . . 7
β’ (π
β Ring β π
β CMnd) |
5 | 3, 4 | syl 17 |
. . . . . 6
β’ (π β π
β CMnd) |
6 | 5 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π·) β π
β CMnd) |
7 | | psrass.d |
. . . . . . 7
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
8 | 7 | psrbaglefi 21485 |
. . . . . 6
β’ (π₯ β π· β {π β π· β£ π βr β€ π₯} β Fin) |
9 | 8 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β π·) β {π β π· β£ π βr β€ π₯} β Fin) |
10 | 3 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π
β Ring) |
11 | | psrring.s |
. . . . . . . . . 10
β’ π = (πΌ mPwSer π
) |
12 | | psrass.b |
. . . . . . . . . 10
β’ π΅ = (Baseβπ) |
13 | | psrass.x |
. . . . . . . . . 10
β’ (π β π β π΅) |
14 | 11, 1, 7, 12, 13 | psrelbas 21498 |
. . . . . . . . 9
β’ (π β π:π·βΆ(Baseβπ
)) |
15 | 14 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:π·βΆ(Baseβπ
)) |
16 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β {π β π· β£ π βr β€ π₯}) |
17 | | breq1 5152 |
. . . . . . . . . . 11
β’ (π = π β (π βr β€ π₯ β π βr β€ π₯)) |
18 | 17 | elrab 3684 |
. . . . . . . . . 10
β’ (π β {π β π· β£ π βr β€ π₯} β (π β π· β§ π βr β€ π₯)) |
19 | 16, 18 | sylib 217 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π β π· β§ π βr β€ π₯)) |
20 | 19 | simpld 496 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π·) |
21 | 15, 20 | ffvelcdmd 7088 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (πβπ) β (Baseβπ
)) |
22 | | psrass.y |
. . . . . . . . . 10
β’ (π β π β π΅) |
23 | 11, 1, 7, 12, 22 | psrelbas 21498 |
. . . . . . . . 9
β’ (π β π:π·βΆ(Baseβπ
)) |
24 | 23 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:π·βΆ(Baseβπ
)) |
25 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π₯ β π·) |
26 | 7 | psrbagf 21471 |
. . . . . . . . . . 11
β’ (π β π· β π:πΌβΆβ0) |
27 | 20, 26 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:πΌβΆβ0) |
28 | 19 | simprd 497 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π βr β€ π₯) |
29 | 7 | psrbagcon 21483 |
. . . . . . . . . 10
β’ ((π₯ β π· β§ π:πΌβΆβ0 β§ π βr β€ π₯) β ((π₯ βf β π) β π· β§ (π₯ βf β π) βr β€ π₯)) |
30 | 25, 27, 28, 29 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π₯ βf β π) β π· β§ (π₯ βf β π) βr β€ π₯)) |
31 | 30 | simpld 496 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π₯ βf β π) β π·) |
32 | 24, 31 | ffvelcdmd 7088 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (πβ(π₯ βf β π)) β (Baseβπ
)) |
33 | | eqid 2733 |
. . . . . . . 8
β’
(.rβπ
) = (.rβπ
) |
34 | 1, 33 | ringcl 20073 |
. . . . . . 7
β’ ((π
β Ring β§ (πβπ) β (Baseβπ
) β§ (πβ(π₯ βf β π)) β (Baseβπ
)) β ((πβπ)(.rβπ
)(πβ(π₯ βf β π))) β (Baseβπ
)) |
35 | 10, 21, 32, 34 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((πβπ)(.rβπ
)(πβ(π₯ βf β π))) β (Baseβπ
)) |
36 | 35 | fmpttd 7115 |
. . . . 5
β’ ((π β§ π₯ β π·) β (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))):{π β π· β£ π βr β€ π₯}βΆ(Baseβπ
)) |
37 | | ovex 7442 |
. . . . . . . . . 10
β’
(β0 βm πΌ) β V |
38 | 7, 37 | rabex2 5335 |
. . . . . . . . 9
β’ π· β V |
39 | 38 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π₯ β π·) β π· β V) |
40 | | rabexg 5332 |
. . . . . . . 8
β’ (π· β V β {π β π· β£ π βr β€ π₯} β V) |
41 | 39, 40 | syl 17 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β {π β π· β£ π βr β€ π₯} β V) |
42 | 41 | mptexd 7226 |
. . . . . 6
β’ ((π β§ π₯ β π·) β (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) β V) |
43 | | funmpt 6587 |
. . . . . . 7
β’ Fun
(π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) |
44 | 43 | a1i 11 |
. . . . . 6
β’ ((π β§ π₯ β π·) β Fun (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π))))) |
45 | | fvexd 6907 |
. . . . . 6
β’ ((π β§ π₯ β π·) β (0gβπ
) β V) |
46 | | suppssdm 8162 |
. . . . . . . 8
β’ ((π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) supp
(0gβπ
))
β dom (π β
{π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) |
47 | | eqid 2733 |
. . . . . . . . 9
β’ (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) = (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) |
48 | 47 | dmmptss 6241 |
. . . . . . . 8
β’ dom
(π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) β {π β π· β£ π βr β€ π₯} |
49 | 46, 48 | sstri 3992 |
. . . . . . 7
β’ ((π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) supp
(0gβπ
))
β {π β π· β£ π βr β€ π₯} |
50 | 49 | a1i 11 |
. . . . . 6
β’ ((π β§ π₯ β π·) β ((π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) supp
(0gβπ
))
β {π β π· β£ π βr β€ π₯}) |
51 | | suppssfifsupp 9378 |
. . . . . 6
β’ ((((π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) β V β§ Fun (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) β§
(0gβπ
)
β V) β§ ({π β
π· β£ π βr β€ π₯} β Fin β§ ((π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) supp
(0gβπ
))
β {π β π· β£ π βr β€ π₯})) β (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) finSupp
(0gβπ
)) |
52 | 42, 44, 45, 9, 50, 51 | syl32anc 1379 |
. . . . 5
β’ ((π β§ π₯ β π·) β (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) finSupp
(0gβπ
)) |
53 | | eqid 2733 |
. . . . . . 7
β’ {π β π· β£ π βr β€ π₯} = {π β π· β£ π βr β€ π₯} |
54 | 7, 53 | psrbagconf1o 21489 |
. . . . . 6
β’ (π₯ β π· β (π β {π β π· β£ π βr β€ π₯} β¦ (π₯ βf β π)):{π β π· β£ π βr β€ π₯}β1-1-ontoβ{π β π· β£ π βr β€ π₯}) |
55 | 54 | adantl 483 |
. . . . 5
β’ ((π β§ π₯ β π·) β (π β {π β π· β£ π βr β€ π₯} β¦ (π₯ βf β π)):{π β π· β£ π βr β€ π₯}β1-1-ontoβ{π β π· β£ π βr β€ π₯}) |
56 | 1, 2, 6, 9, 36, 52, 55 | gsumf1o 19784 |
. . . 4
β’ ((π β§ π₯ β π·) β (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π))))) = (π
Ξ£g ((π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) β (π β {π β π· β£ π βr β€ π₯} β¦ (π₯ βf β π))))) |
57 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π₯ β π·) |
58 | | simpr 486 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β {π β π· β£ π βr β€ π₯}) |
59 | 7, 53 | psrbagconcl 21487 |
. . . . . . . 8
β’ ((π₯ β π· β§ π β {π β π· β£ π βr β€ π₯}) β (π₯ βf β π) β {π β π· β£ π βr β€ π₯}) |
60 | 57, 58, 59 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π₯ βf β π) β {π β π· β£ π βr β€ π₯}) |
61 | | eqidd 2734 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β (π β {π β π· β£ π βr β€ π₯} β¦ (π₯ βf β π)) = (π β {π β π· β£ π βr β€ π₯} β¦ (π₯ βf β π))) |
62 | | eqidd 2734 |
. . . . . . 7
β’ ((π β§ π₯ β π·) β (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) = (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π))))) |
63 | | fveq2 6892 |
. . . . . . . 8
β’ (π = (π₯ βf β π) β (πβπ) = (πβ(π₯ βf β π))) |
64 | | oveq2 7417 |
. . . . . . . . 9
β’ (π = (π₯ βf β π) β (π₯ βf β π) = (π₯ βf β (π₯ βf β
π))) |
65 | 64 | fveq2d 6896 |
. . . . . . . 8
β’ (π = (π₯ βf β π) β (πβ(π₯ βf β π)) = (πβ(π₯ βf β (π₯ βf β
π)))) |
66 | 63, 65 | oveq12d 7427 |
. . . . . . 7
β’ (π = (π₯ βf β π) β ((πβπ)(.rβπ
)(πβ(π₯ βf β π))) = ((πβ(π₯ βf β π))(.rβπ
)(πβ(π₯ βf β (π₯ βf β
π))))) |
67 | 60, 61, 62, 66 | fmptco 7127 |
. . . . . 6
β’ ((π β§ π₯ β π·) β ((π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) β (π β {π β π· β£ π βr β€ π₯} β¦ (π₯ βf β π))) = (π β {π β π· β£ π βr β€ π₯} β¦ ((πβ(π₯ βf β π))(.rβπ
)(πβ(π₯ βf β (π₯ βf β
π)))))) |
68 | 7 | psrbagf 21471 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β π· β π₯:πΌβΆβ0) |
69 | 68 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β π·) β π₯:πΌβΆβ0) |
70 | 69 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π₯:πΌβΆβ0) |
71 | 70 | ffvelcdmda 7087 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π§ β πΌ) β (π₯βπ§) β
β0) |
72 | | breq1 5152 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (π βr β€ π₯ β π βr β€ π₯)) |
73 | 72 | elrab 3684 |
. . . . . . . . . . . . . . . . 17
β’ (π β {π β π· β£ π βr β€ π₯} β (π β π· β§ π βr β€ π₯)) |
74 | 58, 73 | sylib 217 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π β π· β§ π βr β€ π₯)) |
75 | 74 | simpld 496 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π·) |
76 | 7 | psrbagf 21471 |
. . . . . . . . . . . . . . 15
β’ (π β π· β π:πΌβΆβ0) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:πΌβΆβ0) |
78 | 77 | ffvelcdmda 7087 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π§ β πΌ) β (πβπ§) β
β0) |
79 | | nn0cn 12482 |
. . . . . . . . . . . . . 14
β’ ((π₯βπ§) β β0 β (π₯βπ§) β β) |
80 | | nn0cn 12482 |
. . . . . . . . . . . . . 14
β’ ((πβπ§) β β0 β (πβπ§) β β) |
81 | | nncan 11489 |
. . . . . . . . . . . . . 14
β’ (((π₯βπ§) β β β§ (πβπ§) β β) β ((π₯βπ§) β ((π₯βπ§) β (πβπ§))) = (πβπ§)) |
82 | 79, 80, 81 | syl2an 597 |
. . . . . . . . . . . . 13
β’ (((π₯βπ§) β β0 β§ (πβπ§) β β0) β ((π₯βπ§) β ((π₯βπ§) β (πβπ§))) = (πβπ§)) |
83 | 71, 78, 82 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π§ β πΌ) β ((π₯βπ§) β ((π₯βπ§) β (πβπ§))) = (πβπ§)) |
84 | 83 | mpteq2dva 5249 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π§ β πΌ β¦ ((π₯βπ§) β ((π₯βπ§) β (πβπ§)))) = (π§ β πΌ β¦ (πβπ§))) |
85 | | psrring.i |
. . . . . . . . . . . . 13
β’ (π β πΌ β π) |
86 | 85 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β πΌ β π) |
87 | | ovex 7442 |
. . . . . . . . . . . . 13
β’ ((π₯βπ§) β (πβπ§)) β V |
88 | 87 | a1i 11 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π§ β πΌ) β ((π₯βπ§) β (πβπ§)) β V) |
89 | 70 | feqmptd 6961 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π₯ = (π§ β πΌ β¦ (π₯βπ§))) |
90 | 77 | feqmptd 6961 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π = (π§ β πΌ β¦ (πβπ§))) |
91 | 86, 71, 78, 89, 90 | offval2 7690 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π₯ βf β π) = (π§ β πΌ β¦ ((π₯βπ§) β (πβπ§)))) |
92 | 86, 71, 88, 89, 91 | offval2 7690 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π₯ βf β (π₯ βf β
π)) = (π§ β πΌ β¦ ((π₯βπ§) β ((π₯βπ§) β (πβπ§))))) |
93 | 84, 92, 90 | 3eqtr4d 2783 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π₯ βf β (π₯ βf β
π)) = π) |
94 | 93 | fveq2d 6896 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (πβ(π₯ βf β (π₯ βf β
π))) = (πβπ)) |
95 | 94 | oveq2d 7425 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((πβ(π₯ βf β π))(.rβπ
)(πβ(π₯ βf β (π₯ βf β
π)))) = ((πβ(π₯ βf β π))(.rβπ
)(πβπ))) |
96 | | psrcom.c |
. . . . . . . . . 10
β’ (π β π
β CRing) |
97 | 96 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π
β CRing) |
98 | 14 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:π·βΆ(Baseβπ
)) |
99 | 74 | simprd 497 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π βr β€ π₯) |
100 | 7 | psrbagcon 21483 |
. . . . . . . . . . . 12
β’ ((π₯ β π· β§ π:πΌβΆβ0 β§ π βr β€ π₯) β ((π₯ βf β π) β π· β§ (π₯ βf β π) βr β€ π₯)) |
101 | 57, 77, 99, 100 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π₯ βf β π) β π· β§ (π₯ βf β π) βr β€ π₯)) |
102 | 101 | simpld 496 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π₯ βf β π) β π·) |
103 | 98, 102 | ffvelcdmd 7088 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (πβ(π₯ βf β π)) β (Baseβπ
)) |
104 | 23 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:π·βΆ(Baseβπ
)) |
105 | 104, 75 | ffvelcdmd 7088 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (πβπ) β (Baseβπ
)) |
106 | 1, 33 | crngcom 20074 |
. . . . . . . . 9
β’ ((π
β CRing β§ (πβ(π₯ βf β π)) β (Baseβπ
) β§ (πβπ) β (Baseβπ
)) β ((πβ(π₯ βf β π))(.rβπ
)(πβπ)) = ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) |
107 | 97, 103, 105, 106 | syl3anc 1372 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((πβ(π₯ βf β π))(.rβπ
)(πβπ)) = ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) |
108 | 95, 107 | eqtrd 2773 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((πβ(π₯ βf β π))(.rβπ
)(πβ(π₯ βf β (π₯ βf β
π)))) = ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) |
109 | 108 | mpteq2dva 5249 |
. . . . . 6
β’ ((π β§ π₯ β π·) β (π β {π β π· β£ π βr β€ π₯} β¦ ((πβ(π₯ βf β π))(.rβπ
)(πβ(π₯ βf β (π₯ βf β
π))))) = (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π))))) |
110 | 67, 109 | eqtrd 2773 |
. . . . 5
β’ ((π β§ π₯ β π·) β ((π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) β (π β {π β π· β£ π βr β€ π₯} β¦ (π₯ βf β π))) = (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π))))) |
111 | 110 | oveq2d 7425 |
. . . 4
β’ ((π β§ π₯ β π·) β (π
Ξ£g ((π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))) β (π β {π β π· β£ π βr β€ π₯} β¦ (π₯ βf β π)))) = (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))))) |
112 | 56, 111 | eqtrd 2773 |
. . 3
β’ ((π β§ π₯ β π·) β (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π))))) = (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))))) |
113 | 112 | mpteq2dva 5249 |
. 2
β’ (π β (π₯ β π· β¦ (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π)))))) = (π₯ β π· β¦ (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π))))))) |
114 | | psrass.t |
. . 3
β’ Γ =
(.rβπ) |
115 | 11, 12, 33, 114, 7, 13, 22 | psrmulfval 21504 |
. 2
β’ (π β (π Γ π) = (π₯ β π· β¦ (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π))))))) |
116 | 11, 12, 33, 114, 7, 22, 13 | psrmulfval 21504 |
. 2
β’ (π β (π Γ π) = (π₯ β π· β¦ (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)(πβ(π₯ βf β π))))))) |
117 | 113, 115,
116 | 3eqtr4d 2783 |
1
β’ (π β (π Γ π) = (π Γ π)) |