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 21372 |
. . . . 5
β’ (π β (π Γ π) β π΅) |
10 | | psrass.z |
. . . . 5
β’ (π β π β π΅) |
11 | 1, 4, 5, 6, 9, 10 | psrmulcl 21372 |
. . . 4
β’ (π β ((π Γ π) Γ π) β π΅) |
12 | 1, 2, 3, 4, 11 | psrelbas 21363 |
. . 3
β’ (π β ((π Γ π) Γ π):π·βΆ(Baseβπ
)) |
13 | 12 | ffnd 6670 |
. 2
β’ (π β ((π Γ π) Γ π) Fn π·) |
14 | 1, 4, 5, 6, 8, 10 | psrmulcl 21372 |
. . . . 5
β’ (π β (π Γ π) β π΅) |
15 | 1, 4, 5, 6, 7, 14 | psrmulcl 21372 |
. . . 4
β’ (π β (π Γ (π Γ π)) β π΅) |
16 | 1, 2, 3, 4, 15 | psrelbas 21363 |
. . 3
β’ (π β (π Γ (π Γ π)):π·βΆ(Baseβπ
)) |
17 | 16 | ffnd 6670 |
. 2
β’ (π β (π Γ (π Γ π)) Fn π·) |
18 | | eqid 2733 |
. . . . 5
β’ {π β π· β£ π βr β€ π₯} = {π β π· β£ π βr β€ π₯} |
19 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ β π·) β π₯ β π·) |
20 | | ringcmn 20008 |
. . . . . . 7
β’ (π
β Ring β π
β CMnd) |
21 | 6, 20 | syl 17 |
. . . . . 6
β’ (π β π
β CMnd) |
22 | 21 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π·) β π
β CMnd) |
23 | 6 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π
β Ring) |
24 | 23 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π
β Ring) |
25 | 1, 2, 3, 4, 7 | psrelbas 21363 |
. . . . . . . . . 10
β’ (π β π:π·βΆ(Baseβπ
)) |
26 | 25 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:π·βΆ(Baseβπ
)) |
27 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β {π β π· β£ π βr β€ π₯}) |
28 | | breq1 5109 |
. . . . . . . . . . . 12
β’ (π = π β (π βr β€ π₯ β π βr β€ π₯)) |
29 | 28 | elrab 3646 |
. . . . . . . . . . 11
β’ (π β {π β π· β£ π βr β€ π₯} β (π β π· β§ π βr β€ π₯)) |
30 | 27, 29 | sylib 217 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π β π· β§ π βr β€ π₯)) |
31 | 30 | simpld 496 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π·) |
32 | 26, 31 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (πβπ) β (Baseβπ
)) |
33 | 32 | adantr 482 |
. . . . . . 7
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β (πβπ) β (Baseβπ
)) |
34 | 1, 2, 3, 4, 8 | psrelbas 21363 |
. . . . . . . . . 10
β’ (π β π:π·βΆ(Baseβπ
)) |
35 | 34 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π:π·βΆ(Baseβπ
)) |
36 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π β {β β π· β£ β βr β€ (π₯ βf β π)}) |
37 | | breq1 5109 |
. . . . . . . . . . . 12
β’ (β = π β (β βr β€ (π₯ βf β π) β π βr β€ (π₯ βf β π))) |
38 | 37 | elrab 3646 |
. . . . . . . . . . 11
β’ (π β {β β π· β£ β βr β€ (π₯ βf β π)} β (π β π· β§ π βr β€ (π₯ βf β π))) |
39 | 36, 38 | sylib 217 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β (π β π· β§ π βr β€ (π₯ βf β π))) |
40 | 39 | simpld 496 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π β π·) |
41 | 35, 40 | ffvelcdmd 7037 |
. . . . . . . 8
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β (πβπ) β (Baseβπ
)) |
42 | 1, 2, 3, 4, 10 | psrelbas 21363 |
. . . . . . . . . 10
β’ (π β π:π·βΆ(Baseβπ
)) |
43 | 42 | ad3antrrr 729 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π:π·βΆ(Baseβπ
)) |
44 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π₯ β π·) |
45 | 3 | psrbagf 21336 |
. . . . . . . . . . . . . . 15
β’ (π β π· β π:πΌβΆβ0) |
46 | 31, 45 | syl 17 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:πΌβΆβ0) |
47 | 30 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π βr β€ π₯) |
48 | 3 | psrbagcon 21348 |
. . . . . . . . . . . . . 14
β’ ((π₯ β π· β§ π:πΌβΆβ0 β§ π βr β€ π₯) β ((π₯ βf β π) β π· β§ (π₯ βf β π) βr β€ π₯)) |
49 | 44, 46, 47, 48 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π₯ βf β π) β π· β§ (π₯ βf β π) βr β€ π₯)) |
50 | 49 | simpld 496 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π₯ βf β π) β π·) |
51 | 50 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β (π₯ βf β π) β π·) |
52 | 3 | psrbagf 21336 |
. . . . . . . . . . . 12
β’ (π β π· β π:πΌβΆβ0) |
53 | 40, 52 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π:πΌβΆβ0) |
54 | 39 | simprd 497 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β π βr β€ (π₯ βf β π)) |
55 | 3 | psrbagcon 21348 |
. . . . . . . . . . 11
β’ (((π₯ βf β
π) β π· β§ π:πΌβΆβ0 β§ π βr β€ (π₯ βf β
π)) β (((π₯ βf β
π) βf
β π) β π· β§ ((π₯ βf β π) βf β
π) βr β€
(π₯ βf
β π))) |
56 | 51, 53, 54, 55 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β (((π₯ βf β π) βf β
π) β π· β§ ((π₯ βf β π) βf β
π) βr β€
(π₯ βf
β π))) |
57 | 56 | simpld 496 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β ((π₯ βf β π) βf β
π) β π·) |
58 | 43, 57 | ffvelcdmd 7037 |
. . . . . . . 8
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β (πβ((π₯ βf β π) βf β
π)) β
(Baseβπ
)) |
59 | | eqid 2733 |
. . . . . . . . 9
β’
(.rβπ
) = (.rβπ
) |
60 | 2, 59 | ringcl 19986 |
. . . . . . . 8
β’ ((π
β Ring β§ (πβπ) β (Baseβπ
) β§ (πβ((π₯ βf β π) βf β
π)) β
(Baseβπ
)) β
((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))) β
(Baseβπ
)) |
61 | 24, 41, 58, 60 | syl3anc 1372 |
. . . . . . 7
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))) β
(Baseβπ
)) |
62 | 2, 59 | ringcl 19986 |
. . . . . . 7
β’ ((π
β Ring β§ (πβπ) β (Baseβπ
) β§ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))) β
(Baseβπ
)) β
((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β
(Baseβπ
)) |
63 | 24, 33, 61, 62 | syl3anc 1372 |
. . . . . 6
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ (π₯ βf β π)}) β ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β
(Baseβπ
)) |
64 | 63 | anasss 468 |
. . . . 5
β’ (((π β§ π₯ β π·) β§ (π β {π β π· β£ π βr β€ π₯} β§ π β {β β π· β£ β βr β€ (π₯ βf β π)})) β ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β
(Baseβπ
)) |
65 | | fveq2 6843 |
. . . . . . 7
β’ (π = (π βf β π) β (πβπ) = (πβ(π βf β π))) |
66 | | oveq2 7366 |
. . . . . . . 8
β’ (π = (π βf β π) β ((π₯ βf β π) βf β
π) = ((π₯ βf β π) βf β
(π βf
β π))) |
67 | 66 | fveq2d 6847 |
. . . . . . 7
β’ (π = (π βf β π) β (πβ((π₯ βf β π) βf β
π)) = (πβ((π₯ βf β π) βf β
(π βf
β π)))) |
68 | 65, 67 | oveq12d 7376 |
. . . . . 6
β’ (π = (π βf β π) β ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))) = ((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π))))) |
69 | 68 | oveq2d 7374 |
. . . . 5
β’ (π = (π βf β π) β ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) = ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π)))))) |
70 | 3, 18, 19, 2, 22, 64, 69 | psrass1lem 21361 |
. . . 4
β’ ((π β§ π₯ β π·) β (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π))))))))) = (π
Ξ£g
(π β {π β π· β£ π βr β€ π₯} β¦ (π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))))))))) |
71 | 7 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π΅) |
72 | 8 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π΅) |
73 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β {π β π· β£ π βr β€ π₯}) |
74 | | breq1 5109 |
. . . . . . . . . . . 12
β’ (π = π β (π βr β€ π₯ β π βr β€ π₯)) |
75 | 74 | elrab 3646 |
. . . . . . . . . . 11
β’ (π β {π β π· β£ π βr β€ π₯} β (π β π· β§ π βr β€ π₯)) |
76 | 73, 75 | sylib 217 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π β π· β§ π βr β€ π₯)) |
77 | 76 | simpld 496 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π·) |
78 | 1, 4, 59, 5, 3, 71, 72, 77 | psrmulval 21370 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π Γ π)βπ) = (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)(πβ(π βf β π)))))) |
79 | 78 | oveq1d 7373 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (((π Γ π)βπ)(.rβπ
)(πβ(π₯ βf β π))) = ((π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)(πβ(π βf β π)))))(.rβπ
)(πβ(π₯ βf β π)))) |
80 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ
) = (0gβπ
) |
81 | | eqid 2733 |
. . . . . . . 8
β’
(+gβπ
) = (+gβπ
) |
82 | 6 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π
β Ring) |
83 | 3 | psrbaglefi 21350 |
. . . . . . . . 9
β’ (π β π· β {β β π· β£ β βr β€ π} β Fin) |
84 | 77, 83 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β {β β π· β£ β βr β€ π} β Fin) |
85 | 42 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:π·βΆ(Baseβπ
)) |
86 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π₯ β π·) |
87 | 3 | psrbagf 21336 |
. . . . . . . . . . . 12
β’ (π β π· β π:πΌβΆβ0) |
88 | 77, 87 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π:πΌβΆβ0) |
89 | 76 | simprd 497 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π βr β€ π₯) |
90 | 3 | psrbagcon 21348 |
. . . . . . . . . . 11
β’ ((π₯ β π· β§ π:πΌβΆβ0 β§ π βr β€ π₯) β ((π₯ βf β π) β π· β§ (π₯ βf β π) βr β€ π₯)) |
91 | 86, 88, 89, 90 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π₯ βf β π) β π· β§ (π₯ βf β π) βr β€ π₯)) |
92 | 91 | simpld 496 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π₯ βf β π) β π·) |
93 | 85, 92 | ffvelcdmd 7037 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (πβ(π₯ βf β π)) β (Baseβπ
)) |
94 | 82 | adantr 482 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π
β Ring) |
95 | 25 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π:π·βΆ(Baseβπ
)) |
96 | | simpr 486 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π β {β β π· β£ β βr β€ π}) |
97 | | breq1 5109 |
. . . . . . . . . . . . 13
β’ (β = π β (β βr β€ π β π βr β€ π)) |
98 | 97 | elrab 3646 |
. . . . . . . . . . . 12
β’ (π β {β β π· β£ β βr β€ π} β (π β π· β§ π βr β€ π)) |
99 | 96, 98 | sylib 217 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (π β π· β§ π βr β€ π)) |
100 | 99 | simpld 496 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π β π·) |
101 | 95, 100 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (πβπ) β (Baseβπ
)) |
102 | 34 | ad3antrrr 729 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π:π·βΆ(Baseβπ
)) |
103 | 77 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π β π·) |
104 | 100, 45 | syl 17 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π:πΌβΆβ0) |
105 | 99 | simprd 497 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π βr β€ π) |
106 | 3 | psrbagcon 21348 |
. . . . . . . . . . . 12
β’ ((π β π· β§ π:πΌβΆβ0 β§ π βr β€ π) β ((π βf β π) β π· β§ (π βf β π) βr β€ π)) |
107 | 103, 104,
105, 106 | syl3anc 1372 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β ((π βf β π) β π· β§ (π βf β π) βr β€ π)) |
108 | 107 | simpld 496 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (π βf β π) β π·) |
109 | 102, 108 | ffvelcdmd 7037 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (πβ(π βf β π)) β (Baseβπ
)) |
110 | 2, 59 | ringcl 19986 |
. . . . . . . . 9
β’ ((π
β Ring β§ (πβπ) β (Baseβπ
) β§ (πβ(π βf β π)) β (Baseβπ
)) β ((πβπ)(.rβπ
)(πβ(π βf β π))) β (Baseβπ
)) |
111 | 94, 101, 109, 110 | syl3anc 1372 |
. . . . . . . 8
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β ((πβπ)(.rβπ
)(πβ(π βf β π))) β (Baseβπ
)) |
112 | | eqid 2733 |
. . . . . . . . 9
β’ (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)(πβ(π βf β π)))) = (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)(πβ(π βf β π)))) |
113 | | fvex 6856 |
. . . . . . . . . 10
β’
(0gβπ
) β V |
114 | 113 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (0gβπ
) β V) |
115 | 112, 84, 111, 114 | fsuppmptdm 9321 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)(πβ(π βf β π)))) finSupp
(0gβπ
)) |
116 | 2, 80, 81, 59, 82, 84, 93, 111, 115 | gsummulc1 20035 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ (((πβπ)(.rβπ
)(πβ(π βf β π)))(.rβπ
)(πβ(π₯ βf β π))))) = ((π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)(πβ(π βf β π)))))(.rβπ
)(πβ(π₯ βf β π)))) |
117 | 93 | adantr 482 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (πβ(π₯ βf β π)) β (Baseβπ
)) |
118 | 2, 59 | ringass 19989 |
. . . . . . . . . . 11
β’ ((π
β Ring β§ ((πβπ) β (Baseβπ
) β§ (πβ(π βf β π)) β (Baseβπ
) β§ (πβ(π₯ βf β π)) β (Baseβπ
))) β (((πβπ)(.rβπ
)(πβ(π βf β π)))(.rβπ
)(πβ(π₯ βf β π))) = ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ(π₯ βf β π))))) |
119 | 94, 101, 109, 117, 118 | syl13anc 1373 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (((πβπ)(.rβπ
)(πβ(π βf β π)))(.rβπ
)(πβ(π₯ βf β π))) = ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ(π₯ βf β π))))) |
120 | 3 | psrbagf 21336 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β π· β π₯:πΌβΆβ0) |
121 | 120 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β π·) β π₯:πΌβΆβ0) |
122 | 121 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π₯:πΌβΆβ0) |
123 | 122 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β§ π§ β πΌ) β (π₯βπ§) β
β0) |
124 | 88 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π:πΌβΆβ0) |
125 | 124 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β§ π§ β πΌ) β (πβπ§) β
β0) |
126 | 104 | ffvelcdmda 7036 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β§ π§ β πΌ) β (πβπ§) β
β0) |
127 | | nn0cn 12428 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯βπ§) β β0 β (π₯βπ§) β β) |
128 | | nn0cn 12428 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ§) β β0 β (πβπ§) β β) |
129 | | nn0cn 12428 |
. . . . . . . . . . . . . . . . 17
β’ ((πβπ§) β β0 β (πβπ§) β β) |
130 | | nnncan2 11443 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯βπ§) β β β§ (πβπ§) β β β§ (πβπ§) β β) β (((π₯βπ§) β (πβπ§)) β ((πβπ§) β (πβπ§))) = ((π₯βπ§) β (πβπ§))) |
131 | 127, 128,
129, 130 | syl3an 1161 |
. . . . . . . . . . . . . . . 16
β’ (((π₯βπ§) β β0 β§ (πβπ§) β β0 β§ (πβπ§) β β0) β (((π₯βπ§) β (πβπ§)) β ((πβπ§) β (πβπ§))) = ((π₯βπ§) β (πβπ§))) |
132 | 123, 125,
126, 131 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β§ π§ β πΌ) β (((π₯βπ§) β (πβπ§)) β ((πβπ§) β (πβπ§))) = ((π₯βπ§) β (πβπ§))) |
133 | 132 | mpteq2dva 5206 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (π§ β πΌ β¦ (((π₯βπ§) β (πβπ§)) β ((πβπ§) β (πβπ§)))) = (π§ β πΌ β¦ ((π₯βπ§) β (πβπ§)))) |
134 | | psrring.i |
. . . . . . . . . . . . . . . . 17
β’ (π β πΌ β π) |
135 | 134 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β πΌ β π) |
136 | 135 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β πΌ β π) |
137 | | ovexd 7393 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β§ π§ β πΌ) β ((π₯βπ§) β (πβπ§)) β V) |
138 | | ovexd 7393 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β§ π§ β πΌ) β ((πβπ§) β (πβπ§)) β V) |
139 | 122 | feqmptd 6911 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π₯ = (π§ β πΌ β¦ (π₯βπ§))) |
140 | 104 | feqmptd 6911 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π = (π§ β πΌ β¦ (πβπ§))) |
141 | 136, 123,
126, 139, 140 | offval2 7638 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (π₯ βf β π) = (π§ β πΌ β¦ ((π₯βπ§) β (πβπ§)))) |
142 | 124 | feqmptd 6911 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β π = (π§ β πΌ β¦ (πβπ§))) |
143 | 136, 125,
126, 142, 140 | offval2 7638 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (π βf β π) = (π§ β πΌ β¦ ((πβπ§) β (πβπ§)))) |
144 | 136, 137,
138, 141, 143 | offval2 7638 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β ((π₯ βf β π) βf β
(π βf
β π)) = (π§ β πΌ β¦ (((π₯βπ§) β (πβπ§)) β ((πβπ§) β (πβπ§))))) |
145 | 136, 123,
125, 139, 142 | offval2 7638 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (π₯ βf β π) = (π§ β πΌ β¦ ((π₯βπ§) β (πβπ§)))) |
146 | 133, 144,
145 | 3eqtr4d 2783 |
. . . . . . . . . . . . 13
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β ((π₯ βf β π) βf β
(π βf
β π)) = (π₯ βf β
π)) |
147 | 146 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (πβ((π₯ βf β π) βf β
(π βf
β π))) = (πβ(π₯ βf β π))) |
148 | 147 | oveq2d 7374 |
. . . . . . . . . . 11
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β ((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π)))) = ((πβ(π βf β π))(.rβπ
)(πβ(π₯ βf β π)))) |
149 | 148 | oveq2d 7374 |
. . . . . . . . . 10
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π))))) = ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ(π₯ βf β π))))) |
150 | 119, 149 | eqtr4d 2776 |
. . . . . . . . 9
β’ ((((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β§ π β {β β π· β£ β βr β€ π}) β (((πβπ)(.rβπ
)(πβ(π βf β π)))(.rβπ
)(πβ(π₯ βf β π))) = ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π)))))) |
151 | 150 | mpteq2dva 5206 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π β {β β π· β£ β βr β€ π} β¦ (((πβπ)(.rβπ
)(πβ(π βf β π)))(.rβπ
)(πβ(π₯ βf β π)))) = (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π))))))) |
152 | 151 | oveq2d 7374 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ (((πβπ)(.rβπ
)(πβ(π βf β π)))(.rβπ
)(πβ(π₯ βf β π))))) = (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π)))))))) |
153 | 79, 116, 152 | 3eqtr2d 2779 |
. . . . . 6
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (((π Γ π)βπ)(.rβπ
)(πβ(π₯ βf β π))) = (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π)))))))) |
154 | 153 | mpteq2dva 5206 |
. . . . 5
β’ ((π β§ π₯ β π·) β (π β {π β π· β£ π βr β€ π₯} β¦ (((π Γ π)βπ)(.rβπ
)(πβ(π₯ βf β π)))) = (π β {π β π· β£ π βr β€ π₯} β¦ (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π))))))))) |
155 | 154 | oveq2d 7374 |
. . . 4
β’ ((π β§ π₯ β π·) β (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ (((π Γ π)βπ)(.rβπ
)(πβ(π₯ βf β π))))) = (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ (π
Ξ£g (π β {β β π· β£ β βr β€ π} β¦ ((πβπ)(.rβπ
)((πβ(π βf β π))(.rβπ
)(πβ((π₯ βf β π) βf β
(π βf
β π)))))))))) |
156 | 8 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π΅) |
157 | 10 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β π β π΅) |
158 | 1, 4, 59, 5, 3, 156, 157, 50 | psrmulval 21370 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π Γ π)β(π₯ βf β π)) = (π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))))) |
159 | 158 | oveq2d 7374 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((πβπ)(.rβπ
)((π Γ π)β(π₯ βf β π))) = ((πβπ)(.rβπ
)(π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))))))) |
160 | 3 | psrbaglefi 21350 |
. . . . . . . . 9
β’ ((π₯ βf β
π) β π· β {β β π· β£ β βr β€ (π₯ βf β π)} β Fin) |
161 | 50, 160 | syl 17 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β {β β π· β£ β βr β€ (π₯ βf β π)} β Fin) |
162 | | ovex 7391 |
. . . . . . . . . . . . 13
β’
(β0 βm πΌ) β V |
163 | 3, 162 | rab2ex 5293 |
. . . . . . . . . . . 12
β’ {β β π· β£ β βr β€ (π₯ βf β π)} β V |
164 | 163 | mptex 7174 |
. . . . . . . . . . 11
β’ (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β
V |
165 | | funmpt 6540 |
. . . . . . . . . . 11
β’ Fun
(π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) |
166 | 164, 165,
113 | 3pm3.2i 1340 |
. . . . . . . . . 10
β’ ((π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β V β§ Fun
(π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β§
(0gβπ
)
β V) |
167 | 166 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β V β§ Fun
(π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β§
(0gβπ
)
β V)) |
168 | | suppssdm 8109 |
. . . . . . . . . . 11
β’ ((π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) supp
(0gβπ
))
β dom (π β
{β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) |
169 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) = (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) |
170 | 169 | dmmptss 6194 |
. . . . . . . . . . 11
β’ dom
(π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) β {β β π· β£ β βr β€ (π₯ βf β π)} |
171 | 168, 170 | sstri 3954 |
. . . . . . . . . 10
β’ ((π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) supp
(0gβπ
))
β {β β π· β£ β βr β€ (π₯ βf β π)} |
172 | 171 | a1i 11 |
. . . . . . . . 9
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) supp
(0gβπ
))
β {β β π· β£ β βr β€ (π₯ βf β π)}) |
173 | | suppssfifsupp 9325 |
. . . . . . . . 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βπ
)) |
174 | 167, 161,
172, 173 | syl12anc 836 |
. . . . . . . 8
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))) finSupp
(0gβπ
)) |
175 | 2, 80, 81, 59, 23, 161, 32, 61, 174 | gsummulc2 20036 |
. . . . . . 7
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β (π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))))) = ((πβπ)(.rβπ
)(π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))))))) |
176 | 159, 175 | eqtr4d 2776 |
. . . . . 6
β’ (((π β§ π₯ β π·) β§ π β {π β π· β£ π βr β€ π₯}) β ((πβπ)(.rβπ
)((π Γ π)β(π₯ βf β π))) = (π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))))))) |
177 | 176 | mpteq2dva 5206 |
. . . . 5
β’ ((π β§ π₯ β π·) β (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)((π Γ π)β(π₯ βf β π)))) = (π β {π β π· β£ π βr β€ π₯} β¦ (π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π)))))))) |
178 | 177 | oveq2d 7374 |
. . . 4
β’ ((π β§ π₯ β π·) β (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)((π Γ π)β(π₯ βf β π))))) = (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ (π
Ξ£g (π β {β β π· β£ β βr β€ (π₯ βf β π)} β¦ ((πβπ)(.rβπ
)((πβπ)(.rβπ
)(πβ((π₯ βf β π) βf β
π))))))))) |
179 | 70, 155, 178 | 3eqtr4d 2783 |
. . 3
β’ ((π β§ π₯ β π·) β (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ (((π Γ π)βπ)(.rβπ
)(πβ(π₯ βf β π))))) = (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)((π Γ π)β(π₯ βf β π)))))) |
180 | 9 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π·) β (π Γ π) β π΅) |
181 | 10 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π·) β π β π΅) |
182 | 1, 4, 59, 5, 3, 180, 181, 19 | psrmulval 21370 |
. . 3
β’ ((π β§ π₯ β π·) β (((π Γ π) Γ π)βπ₯) = (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ (((π Γ π)βπ)(.rβπ
)(πβ(π₯ βf β π)))))) |
183 | 7 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π·) β π β π΅) |
184 | 14 | adantr 482 |
. . . 4
β’ ((π β§ π₯ β π·) β (π Γ π) β π΅) |
185 | 1, 4, 59, 5, 3, 183, 184, 19 | psrmulval 21370 |
. . 3
β’ ((π β§ π₯ β π·) β ((π Γ (π Γ π))βπ₯) = (π
Ξ£g (π β {π β π· β£ π βr β€ π₯} β¦ ((πβπ)(.rβπ
)((π Γ π)β(π₯ βf β π)))))) |
186 | 179, 182,
185 | 3eqtr4d 2783 |
. 2
β’ ((π β§ π₯ β π·) β (((π Γ π) Γ π)βπ₯) = ((π Γ (π Γ π))βπ₯)) |
187 | 13, 17, 186 | eqfnfvd 6986 |
1
β’ (π β ((π Γ π) Γ π) = (π Γ (π Γ π))) |