Step | Hyp | Ref
| Expression |
1 | | psrring.s |
. . . 4
β’ π = (πΌ mPwSer π
) |
2 | | eqid 2733 |
. . . 4
β’
(Baseβπ
) =
(Baseβπ
) |
3 | | psrass.d |
. . . 4
β’ π· = {π β (β0
βm πΌ)
β£ (β‘π β β) β
Fin} |
4 | | psrass.b |
. . . 4
β’ π΅ = (Baseβπ) |
5 | | psrass.t |
. . . . 5
β’ Γ =
(.rβπ) |
6 | | psrring.r |
. . . . 5
β’ (π β π
β Ring) |
7 | | psrass.x |
. . . . . 6
β’ (π β π β π΅) |
8 | | psrass.y |
. . . . . 6
β’ (π β π β π΅) |
9 | 1, 4, 5, 6, 7, 8 | psrmulcl 21507 |
. . . . 5
β’ (π β (π Γ π) β π΅) |
10 | | psrass.z |
. . . . 5
β’ (π β π β π΅) |
11 | 1, 4, 5, 6, 9, 10 | psrmulcl 21507 |
. . . 4
β’ (π β ((π Γ π) Γ π) β π΅) |
12 | 1, 2, 3, 4, 11 | psrelbas 21498 |
. . 3
β’ (π β ((π Γ π) Γ π):π·βΆ(Baseβπ
)) |
13 | 12 | ffnd 6719 |
. 2
β’ (π β ((π Γ π) Γ π) Fn π·) |
14 | 1, 4, 5, 6, 8, 10 | psrmulcl 21507 |
. . . . 5
β’ (π β (π Γ π) β π΅) |
15 | 1, 4, 5, 6, 7, 14 | psrmulcl 21507 |
. . . 4
β’ (π β (π Γ (π Γ π)) β π΅) |
16 | 1, 2, 3, 4, 15 | psrelbas 21498 |
. . 3
β’ (π β (π Γ (π Γ π)):π·βΆ(Baseβπ
)) |
17 | 16 | ffnd 6719 |
. 2
β’ (π β (π Γ (π Γ π)) Fn π·) |
18 | | eqid 2733 |
. . . . 5
β’ {π β π· β£ π βr β€ π₯} = {π β π· β£ π βr β€ π₯} |
19 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ β π·) β π₯ β π·) |
20 | 6 | ringcmnd 20101 |
. . . . . 6
β’ (π β π
β CMnd) |
21 | 20 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π·) β π
β CMnd) |
22 | | eqid 2733 |
. . . . . . 7
β’
(.rβπ
) = (.rβπ
) |
23 | 6 | ad3antrrr 729 |
. . . . . . 7
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π
β Ring) |
24 | 1, 2, 3, 4, 7 | psrelbas 21498 |
. . . . . . . . . 10
β’ (π β π:π·βΆ(Baseβπ
)) |
25 | 24 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:π·βΆ(Baseβπ
)) |
26 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β {π β π· β£ π βr β€ π₯}) |
27 | | breq1 5152 |
. . . . . . . . . . . 12
β’ (π = π β (π βr β€ π₯ β π βr β€ π₯)) |
28 | 27 | elrab 3684 |
. . . . . . . . . . 11
β’ (π β {π β π· β£ π βr β€ π₯} β (π β π· β§ π βr β€ π₯)) |
29 | 26, 28 | sylib 217 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π β π· β§ π βr β€ π₯)) |
30 | 29 | simpld 496 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π·) |
31 | 25, 30 | ffvelcdmd 7088 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (πβπ) β (Baseβπ
)) |
32 | 31 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β (πβπ) β (Baseβπ
)) |
33 | 1, 2, 3, 4, 8 | psrelbas 21498 |
. . . . . . . . . 10
β’ (π β π:π·βΆ(Baseβπ
)) |
34 | 33 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π:π·βΆ(Baseβπ
)) |
35 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π β {β β π· β£ β βr β€ (π₯ βf β π)}) |
36 | | breq1 5152 |
. . . . . . . . . . . 12
β’ (β = π β (β βr β€ (π₯ βf β π) β π βr β€ (π₯ βf β π))) |
37 | 36 | elrab 3684 |
. . . . . . . . . . 11
β’ (π β {β β π· β£ β βr β€ (π₯ βf β π)} β (π β π· β§ π βr β€ (π₯ βf β π))) |
38 | 35, 37 | sylib 217 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β (π β π· β§ π βr β€ (π₯ βf β π))) |
39 | 38 | simpld 496 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π β π·) |
40 | 34, 39 | ffvelcdmd 7088 |
. . . . . . . 8
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β (πβπ) β (Baseβπ
)) |
41 | 1, 2, 3, 4, 10 | psrelbas 21498 |
. . . . . . . . . 10
β’ (π β π:π·βΆ(Baseβπ
)) |
42 | 41 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π:π·βΆ(Baseβπ
)) |
43 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π₯ β π·) |
44 | 3 | psrbagf 21471 |
. . . . . . . . . . . . . . 15
β’ (π β π· β π:πΌβΆβ0) |
45 | 30, 44 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:πΌβΆβ0) |
46 | 29 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π βr β€ π₯) |
47 | 3 | psrbagcon 21483 |
. . . . . . . . . . . . . 14
β’ ((π₯ β π· β§ π:πΌβΆβ0 β§ π βr β€ π₯) β ((π₯ βf β π) β π· β§ (π₯ βf β π) βr β€ π₯)) |
48 | 43, 45, 46, 47 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π₯ βf β π) β π· β§ (π₯ βf β π) βr β€ π₯)) |
49 | 48 | simpld 496 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π₯ βf β π) β π·) |
50 | 49 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β (π₯ βf β π) β π·) |
51 | 3 | psrbagf 21471 |
. . . . . . . . . . . 12
β’ (π β π· β π:πΌβΆβ0) |
52 | 39, 51 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π:πΌβΆβ0) |
53 | 38 | simprd 497 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π βr β€ (π₯ βf β π)) |
54 | 3 | psrbagcon 21483 |
. . . . . . . . . . 11
β’ (((π₯ βf β
π) β π· β§ π:πΌβΆβ0 β§ π βr β€ (π₯ βf β
π)) β (((π₯ βf β
π) βf
β π) β π· β§ ((π₯ βf β π) βf β
π) βr β€
(π₯ βf
β π))) |
55 | 50, 52, 53, 54 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β (((π₯ βf β π) βf β
π) β π· β§ ((π₯ βf β π) βf β
π) βr β€
(π₯ βf
β π))) |
56 | 55 | simpld 496 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β ((π₯ βf β π) βf β
π) β π·) |
57 | 42, 56 | ffvelcdmd 7088 |
. . . . . . . 8
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β (πβ((π₯ βf β π) βf β
π)) β
(Baseβπ
)) |
58 | 2, 22, 23, 40, 57 | ringcld 20080 |
. . . . . . 7
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))) β
(Baseβπ
)) |
59 | 2, 22, 23, 32, 58 | ringcld 20080 |
. . . . . 6
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β
(Baseβπ
)) |
60 | 59 | anasss 468 |
. . . . 5
β’ (((π β§ π₯ β π·) β§ (π β {π β π· β£ π βr β€ π₯} β§ π β {β β π· β£ β βr β€ (π₯ βf β π)})) β ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β
(Baseβπ
)) |
61 | | fveq2 6892 |
. . . . . . 7
β’ (π = (π βf β π) β (πβπ) = (πβ(π βf β π))) |
62 | | oveq2 7417 |
. . . . . . . 8
β’ (π = (π βf β π) β ((π₯ βf β π) βf β
π) = ((π₯ βf β π) βf β
(π βf
β π))) |
63 | 62 | fveq2d 6896 |
. . . . . . 7
β’ (π = (π βf β π) β (πβ((π₯ βf β π) βf β
π)) = (πβ((π₯ βf β π) βf β
(π βf
β π)))) |
64 | 61, 63 | oveq12d 7427 |
. . . . . 6
β’ (π = (π βf β π) β ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))) = ((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π))))) |
65 | 64 | oveq2d 7425 |
. . . . 5
β’ (π = (π βf β π) β ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) = ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π)))))) |
66 | 3, 18, 19, 2, 21, 60, 65 | psrass1lem 21496 |
. . . 4
β’ ((π β§ π₯ β π·) β (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π))))))))) = (π
Ξ£g
(π β {π β π· β£ π βr β€ π₯} β¦ (π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))))))))) |
67 | 7 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π΅) |
68 | 8 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π΅) |
69 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β {π β π· β£ π βr β€ π₯}) |
70 | | breq1 5152 |
. . . . . . . . . . . 12
β’ (π = π β (π βr β€ π₯ β π βr β€ π₯)) |
71 | 70 | elrab 3684 |
. . . . . . . . . . 11
β’ (π β {π β π· β£ π βr β€ π₯} β (π β π· β§ π βr β€ π₯)) |
72 | 69, 71 | sylib 217 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π β π· β§ π βr β€ π₯)) |
73 | 72 | simpld 496 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π·) |
74 | 1, 4, 22, 5, 3, 67, 68, 73 | psrmulval 21505 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π Γ π)βπ) = (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)(πβ(π βf β π)))))) |
75 | 74 | oveq1d 7424 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (((π Γ π)βπ)(.rβπ
)(πβ(π₯ βf β π))) = ((π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)(πβ(π βf β π)))))(.rβπ
)(πβ(π₯ βf β π)))) |
76 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ
) = (0gβπ
) |
77 | 6 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π
β Ring) |
78 | 3 | psrbaglefi 21485 |
. . . . . . . . 9
β’ (π β π· β {β β π· β£ β βr β€ π} β Fin) |
79 | 73, 78 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β {β β π· β£ β βr β€ π} β Fin) |
80 | 41 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:π·βΆ(Baseβπ
)) |
81 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π₯ β π·) |
82 | 3 | psrbagf 21471 |
. . . . . . . . . . . 12
β’ (π β π· β π:πΌβΆβ0) |
83 | 73, 82 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:πΌβΆβ0) |
84 | 72 | simprd 497 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π βr β€ π₯) |
85 | 3 | psrbagcon 21483 |
. . . . . . . . . . 11
β’ ((π₯ β π· β§ π:πΌβΆβ0 β§ π βr β€ π₯) β ((π₯ βf β π) β π· β§ (π₯ βf β π) βr β€ π₯)) |
86 | 81, 83, 84, 85 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π₯ βf β π) β π· β§ (π₯ βf β π) βr β€ π₯)) |
87 | 86 | simpld 496 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π₯ βf β π) β π·) |
88 | 80, 87 | ffvelcdmd 7088 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (πβ(π₯ βf β π)) β (Baseβπ
)) |
89 | 6 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π
β Ring) |
90 | 24 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π:π·βΆ(Baseβπ
)) |
91 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π β {β β π· β£ β βr β€ π}) |
92 | | breq1 5152 |
. . . . . . . . . . . . 13
β’ (β = π β (β βr β€ π β π βr β€ π)) |
93 | 92 | elrab 3684 |
. . . . . . . . . . . 12
β’ (π β {β β π· β£ β βr β€ π} β (π β π· β§ π βr β€ π)) |
94 | 91, 93 | sylib 217 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (π β π· β§ π βr β€ π)) |
95 | 94 | simpld 496 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π β π·) |
96 | 90, 95 | ffvelcdmd 7088 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (πβπ) β (Baseβπ
)) |
97 | 33 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π:π·βΆ(Baseβπ
)) |
98 | 73 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π β π·) |
99 | 95, 44 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π:πΌβΆβ0) |
100 | 94 | simprd 497 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π βr β€ π) |
101 | 3 | psrbagcon 21483 |
. . . . . . . . . . . 12
β’ ((π β π· β§ π:πΌβΆβ0 β§ π βr β€ π) β ((π βf β π) β π· β§ (π βf β π) βr β€ π)) |
102 | 98, 99, 100, 101 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β ((π βf β π) β π· β§ (π βf β π) βr β€ π)) |
103 | 102 | simpld 496 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (π βf β π) β π·) |
104 | 97, 103 | ffvelcdmd 7088 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (πβ(π βf β π)) β (Baseβπ
)) |
105 | 2, 22, 89, 96, 104 | ringcld 20080 |
. . . . . . . 8
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β ((πβπ)(.rβπ
)(πβ(π βf β π))) β (Baseβπ
)) |
106 | | eqid 2733 |
. . . . . . . . 9
β’ (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)(πβ(π βf β π)))) = (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)(πβ(π βf β π)))) |
107 | | fvex 6905 |
. . . . . . . . . 10
β’
(0gβπ
) β V |
108 | 107 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (0gβπ
) β V) |
109 | 106, 79, 105, 108 | fsuppmptdm 9374 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)(πβ(π βf β π)))) finSupp
(0gβπ
)) |
110 | 2, 76, 22, 77, 79, 88, 105, 109 | gsummulc1 20128 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ (((πβπ)(.rβπ
)(πβ(π βf β π)))(.rβπ
)(πβ(π₯ βf β π))))) = ((π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)(πβ(π βf β π)))))(.rβπ
)(πβ(π₯ βf β π)))) |
111 | 88 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (πβ(π₯ βf β π)) β (Baseβπ
)) |
112 | 2, 22 | ringass 20076 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ ((πβπ) β (Baseβπ
) β§ (πβ(π βf β π)) β (Baseβπ
) β§ (πβ(π₯ βf β π)) β (Baseβπ
))) β (((πβπ)(.rβπ
)(πβ(π βf β π)))(.rβπ
)(πβ(π₯ βf β π))) = ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ(π₯ βf β π))))) |
113 | 89, 96, 104, 111, 112 | syl13anc 1373 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (((πβπ)(.rβπ
)(πβ(π βf β π)))(.rβπ
)(πβ(π₯ βf β π))) = ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ(π₯ βf β π))))) |
114 | 3 | psrbagf 21471 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β π· β π₯:πΌβΆβ0) |
115 | 114 | ad3antlr 730 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π₯:πΌβΆβ0) |
116 | 115 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β§ π§ β πΌ) β (π₯βπ§) β
β0) |
117 | 83 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π:πΌβΆβ0) |
118 | 117 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β§ π§ β πΌ) β (πβπ§) β
β0) |
119 | 99 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β§ π§ β πΌ) β (πβπ§) β
β0) |
120 | | nn0cn 12482 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯βπ§) β β0 β (π₯βπ§) β β) |
121 | | nn0cn 12482 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ§) β β0 β (πβπ§) β β) |
122 | | nn0cn 12482 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ§) β β0 β (πβπ§) β β) |
123 | | nnncan2 11497 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯βπ§) β β β§ (πβπ§) β β β§ (πβπ§) β β) β (((π₯βπ§) β (πβπ§)) β ((πβπ§) β (πβπ§))) = ((π₯βπ§) β (πβπ§))) |
124 | 120, 121,
122, 123 | syl3an 1161 |
. . . . . . . . . . . . . . . 16
β’ (((π₯βπ§) β β0 β§ (πβπ§) β β0 β§ (πβπ§) β β0) β (((π₯βπ§) β (πβπ§)) β ((πβπ§) β (πβπ§))) = ((π₯βπ§) β (πβπ§))) |
125 | 116, 118,
119, 124 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β§ π§ β πΌ) β (((π₯βπ§) β (πβπ§)) β ((πβπ§) β (πβπ§))) = ((π₯βπ§) β (πβπ§))) |
126 | 125 | mpteq2dva 5249 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (π§ β πΌ β¦ (((π₯βπ§) β (πβπ§)) β ((πβπ§) β (πβπ§)))) = (π§ β πΌ β¦ ((π₯βπ§) β (πβπ§)))) |
127 | | psrring.i |
. . . . . . . . . . . . . . . 16
β’ (π β πΌ β π) |
128 | 127 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β πΌ β π) |
129 | | ovexd 7444 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β§ π§ β πΌ) β ((π₯βπ§) β (πβπ§)) β V) |
130 | | ovexd 7444 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β§ π§ β πΌ) β ((πβπ§) β (πβπ§)) β V) |
131 | 115 | feqmptd 6961 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π₯ = (π§ β πΌ β¦ (π₯βπ§))) |
132 | 99 | feqmptd 6961 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π = (π§ β πΌ β¦ (πβπ§))) |
133 | 128, 116,
119, 131, 132 | offval2 7690 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (π₯ βf β π) = (π§ β πΌ β¦ ((π₯βπ§) β (πβπ§)))) |
134 | 117 | feqmptd 6961 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π = (π§ β πΌ β¦ (πβπ§))) |
135 | 128, 118,
119, 134, 132 | offval2 7690 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (π βf β π) = (π§ β πΌ β¦ ((πβπ§) β (πβπ§)))) |
136 | 128, 129,
130, 133, 135 | offval2 7690 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β ((π₯ βf β π) βf β
(π βf
β π)) = (π§ β πΌ β¦ (((π₯βπ§) β (πβπ§)) β ((πβπ§) β (πβπ§))))) |
137 | 128, 116,
118, 131, 134 | offval2 7690 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (π₯ βf β π) = (π§ β πΌ β¦ ((π₯βπ§) β (πβπ§)))) |
138 | 126, 136,
137 | 3eqtr4d 2783 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β ((π₯ βf β π) βf β
(π βf
β π)) = (π₯ βf β
π)) |
139 | 138 | fveq2d 6896 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (πβ((π₯ βf β π) βf β
(π βf
β π))) = (πβ(π₯ βf β π))) |
140 | 139 | oveq2d 7425 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β ((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π)))) = ((πβ(π βf β π))(.rβπ
)(πβ(π₯ βf β π)))) |
141 | 140 | oveq2d 7425 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π))))) = ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ(π₯ βf β π))))) |
142 | 113, 141 | eqtr4d 2776 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (((πβπ)(.rβπ
)(πβ(π βf β π)))(.rβπ
)(πβ(π₯ βf β π))) = ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π)))))) |
143 | 142 | mpteq2dva 5249 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π β {β β π· β£ β βr β€ π} β¦ (((πβπ)(.rβπ
)(πβ(π βf β π)))(.rβπ
)(πβ(π₯ βf β π)))) = (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π))))))) |
144 | 143 | oveq2d 7425 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ (((πβπ)(.rβπ
)(πβ(π βf β π)))(.rβπ
)(πβ(π₯ βf β π))))) = (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π)))))))) |
145 | 75, 110, 144 | 3eqtr2d 2779 |
. . . . . 6
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (((π Γ π)βπ)(.rβπ
)(πβ(π₯ βf β π))) = (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π)))))))) |
146 | 145 | mpteq2dva 5249 |
. . . . 5
β’ ((π β§ π₯ β π·) β (π β {π β π· β£ π βr β€ π₯} β¦ (((π Γ π)βπ)(.rβπ
)(πβ(π₯ βf β π)))) = (π β {π β π· β£ π βr β€ π₯} β¦ (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π))))))))) |
147 | 146 | oveq2d 7425 |
. . . 4
β’ ((π β§ π₯ β π·) β (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ (((π Γ π)βπ)(.rβπ
)(πβ(π₯ βf β π))))) = (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π)))))))))) |
148 | 8 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π΅) |
149 | 10 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π΅) |
150 | 1, 4, 22, 5, 3, 148, 149, 49 | psrmulval 21505 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π Γ π)β(π₯ βf β π)) = (π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))))) |
151 | 150 | oveq2d 7425 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((πβπ)(.rβπ
)((π Γ π)β(π₯ βf β π))) = ((πβπ)(.rβπ
)(π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))))))) |
152 | 6 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π
β Ring) |
153 | 3 | psrbaglefi 21485 |
. . . . . . . . 9
β’ ((π₯ βf β
π) β π· β {β β π· β£ β βr β€ (π₯ βf β π)} β Fin) |
154 | 49, 153 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β {β β π· β£ β βr β€ (π₯ βf β π)} β Fin) |
155 | | ovex 7442 |
. . . . . . . . . . . . 13
β’
(β0 βm πΌ) β V |
156 | 3, 155 | rab2ex 5336 |
. . . . . . . . . . . 12
β’ {β β π· β£ β βr β€ (π₯ βf β π)} β V |
157 | 156 | mptex 7225 |
. . . . . . . . . . 11
β’ (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β
V |
158 | | funmpt 6587 |
. . . . . . . . . . 11
β’ Fun
(π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) |
159 | 157, 158,
107 | 3pm3.2i 1340 |
. . . . . . . . . 10
β’ ((π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β V β§ Fun
(π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β§
(0gβπ
)
β V) |
160 | 159 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β V β§ Fun
(π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β§
(0gβπ
)
β V)) |
161 | | suppssdm 8162 |
. . . . . . . . . . 11
β’ ((π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) supp
(0gβπ
))
β dom (π β
{β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) |
162 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) = (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) |
163 | 162 | dmmptss 6241 |
. . . . . . . . . . 11
β’ dom
(π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β {β β π· β£ β βr β€ (π₯ βf β π)} |
164 | 161, 163 | sstri 3992 |
. . . . . . . . . 10
β’ ((π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) supp
(0gβπ
))
β {β β π· β£ β βr β€ (π₯ βf β π)} |
165 | 164 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) supp
(0gβπ
))
β {β β π· β£ β βr β€ (π₯ βf β π)}) |
166 | | suppssfifsupp 9378 |
. . . . . . . . 9
β’ ((((π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β V β§ Fun
(π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β§
(0gβπ
)
β V) β§ ({β β
π· β£ β βr β€ (π₯ βf β
π)} β Fin β§
((π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) supp
(0gβπ
))
β {β β π· β£ β βr β€ (π₯ βf β π)})) β (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) finSupp
(0gβπ
)) |
167 | 160, 154,
165, 166 | syl12anc 836 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) finSupp
(0gβπ
)) |
168 | 2, 76, 22, 152, 154, 31, 58, 167 | gsummulc2 20129 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))))) = ((πβπ)(.rβπ
)(π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))))))) |
169 | 151, 168 | eqtr4d 2776 |
. . . . . 6
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((πβπ)(.rβπ
)((π Γ π)β(π₯ βf β π))) = (π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))))))) |
170 | 169 | mpteq2dva 5249 |
. . . . 5
β’ ((π β§ π₯ β π·) β (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)((π Γ π)β(π₯ βf β π)))) = (π β {π β π· β£ π βr β€ π₯} β¦ (π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))))))) |
171 | 170 | oveq2d 7425 |
. . . 4
β’ ((π β§ π₯ β π·) β (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)((π Γ π)β(π₯ βf β π))))) = (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ (π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))))))))) |
172 | 66, 147, 171 | 3eqtr4d 2783 |
. . 3
β’ ((π β§ π₯ β π·) β (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ (((π Γ π)βπ)(.rβπ
)(πβ(π₯ βf β π))))) = (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)((π Γ π)β(π₯ βf β π)))))) |
173 | 9 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π·) β (π Γ π) β π΅) |
174 | 10 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π·) β π β π΅) |
175 | 1, 4, 22, 5, 3, 173, 174, 19 | psrmulval 21505 |
. . 3
β’ ((π β§ π₯ β π·) β (((π Γ π) Γ π)βπ₯) = (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ (((π Γ π)βπ)(.rβπ
)(πβ(π₯ βf β π)))))) |
176 | 7 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π·) β π β π΅) |
177 | 14 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π·) β (π Γ π) β π΅) |
178 | 1, 4, 22, 5, 3, 176, 177, 19 | psrmulval 21505 |
. . 3
β’ ((π β§ π₯ β π·) β ((π Γ (π Γ π))βπ₯) = (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)((π Γ π)β(π₯ βf β π)))))) |
179 | 172, 175,
178 | 3eqtr4d 2783 |
. 2
β’ ((π β§ π₯ β π·) β (((π Γ π) Γ π)βπ₯) = ((π Γ (π Γ π))βπ₯)) |
180 | 13, 17, 179 | eqfnfvd 7036 |
1
β’ (π β ((π Γ π) Γ π) = (π Γ (π Γ π))) |