Step | Hyp | Ref
| Expression |
1 | | psrring.s |
. . . . . . . . 9
โข ๐ = (๐ผ mPwSer ๐
) |
2 | | psrass23l.n |
. . . . . . . . 9
โข ยท = (
ยท๐ โ๐) |
3 | | eqid 2733 |
. . . . . . . . 9
โข
(Baseโ๐
) =
(Baseโ๐
) |
4 | | psrass.b |
. . . . . . . . 9
โข ๐ต = (Baseโ๐) |
5 | | eqid 2733 |
. . . . . . . . 9
โข
(.rโ๐
) = (.rโ๐
) |
6 | | psrass.d |
. . . . . . . . 9
โข ๐ท = {๐ โ (โ0
โm ๐ผ)
โฃ (โก๐ โ โ) โ
Fin} |
7 | | psrass23l.a |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ ๐พ) |
8 | 7 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ท) โ ๐ด โ ๐พ) |
9 | | psrass23l.k |
. . . . . . . . . . 11
โข ๐พ = (Baseโ๐
) |
10 | 8, 9 | eleqtrdi 2844 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ท) โ ๐ด โ (Baseโ๐
)) |
11 | 10 | adantr 482 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐ด โ (Baseโ๐
)) |
12 | | psrass.x |
. . . . . . . . . 10
โข (๐ โ ๐ โ ๐ต) |
13 | 12 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐ โ ๐ต) |
14 | | ssrab2 4038 |
. . . . . . . . . 10
โข {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โ ๐ท |
15 | | simpr 486 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) |
16 | 14, 15 | sselid 3943 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐ฅ โ ๐ท) |
17 | 1, 2, 3, 4, 5, 6, 11, 13, 16 | psrvscaval 21376 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ((๐ด ยท ๐)โ๐ฅ) = (๐ด(.rโ๐
)(๐โ๐ฅ))) |
18 | 17 | oveq1d 7373 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ (((๐ด ยท ๐)โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))) = ((๐ด(.rโ๐
)(๐โ๐ฅ))(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) |
19 | | psrring.r |
. . . . . . . . 9
โข (๐ โ ๐
โ Ring) |
20 | 19 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐
โ Ring) |
21 | 1, 3, 6, 4, 13 | psrelbas 21363 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐:๐ทโถ(Baseโ๐
)) |
22 | 21, 16 | ffvelcdmd 7037 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ (๐โ๐ฅ) โ (Baseโ๐
)) |
23 | | psrass.y |
. . . . . . . . . . 11
โข (๐ โ ๐ โ ๐ต) |
24 | 23 | ad2antrr 725 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐ โ ๐ต) |
25 | 1, 3, 6, 4, 24 | psrelbas 21363 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐:๐ทโถ(Baseโ๐
)) |
26 | | simplr 768 |
. . . . . . . . . . 11
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ๐ โ ๐ท) |
27 | | eqid 2733 |
. . . . . . . . . . . 12
โข {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} = {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} |
28 | 6, 27 | psrbagconcl 21352 |
. . . . . . . . . . 11
โข ((๐ โ ๐ท โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ (๐ โf โ ๐ฅ) โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) |
29 | 26, 15, 28 | syl2anc 585 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ (๐ โf โ ๐ฅ) โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) |
30 | 14, 29 | sselid 3943 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ (๐ โf โ ๐ฅ) โ ๐ท) |
31 | 25, 30 | ffvelcdmd 7037 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ (๐โ(๐ โf โ ๐ฅ)) โ (Baseโ๐
)) |
32 | 3, 5 | ringass 19989 |
. . . . . . . 8
โข ((๐
โ Ring โง (๐ด โ (Baseโ๐
) โง (๐โ๐ฅ) โ (Baseโ๐
) โง (๐โ(๐ โf โ ๐ฅ)) โ (Baseโ๐
))) โ ((๐ด(.rโ๐
)(๐โ๐ฅ))(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))) = (๐ด(.rโ๐
)((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))) |
33 | 20, 11, 22, 31, 32 | syl13anc 1373 |
. . . . . . 7
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ((๐ด(.rโ๐
)(๐โ๐ฅ))(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))) = (๐ด(.rโ๐
)((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))) |
34 | 18, 33 | eqtrd 2773 |
. . . . . 6
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ (((๐ด ยท ๐)โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))) = (๐ด(.rโ๐
)((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))) |
35 | 34 | mpteq2dva 5206 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ (((๐ด ยท ๐)โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) = (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ (๐ด(.rโ๐
)((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))))) |
36 | 35 | oveq2d 7374 |
. . . 4
โข ((๐ โง ๐ โ ๐ท) โ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ (((๐ด ยท ๐)โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))) = (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ (๐ด(.rโ๐
)((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))))) |
37 | | eqid 2733 |
. . . . 5
โข
(0gโ๐
) = (0gโ๐
) |
38 | | eqid 2733 |
. . . . 5
โข
(+gโ๐
) = (+gโ๐
) |
39 | 19 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ ๐
โ Ring) |
40 | 6 | psrbaglefi 21350 |
. . . . . 6
โข (๐ โ ๐ท โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โ Fin) |
41 | 40 | adantl 483 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โ Fin) |
42 | 3, 5 | ringcl 19986 |
. . . . . 6
โข ((๐
โ Ring โง (๐โ๐ฅ) โ (Baseโ๐
) โง (๐โ(๐ โf โ ๐ฅ)) โ (Baseโ๐
)) โ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))) โ (Baseโ๐
)) |
43 | 20, 22, 31, 42 | syl3anc 1372 |
. . . . 5
โข (((๐ โง ๐ โ ๐ท) โง ๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) โ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))) โ (Baseโ๐
)) |
44 | | ovex 7391 |
. . . . . . . . . 10
โข
(โ0 โm ๐ผ) โ V |
45 | 6, 44 | rabex2 5292 |
. . . . . . . . 9
โข ๐ท โ V |
46 | 45 | mptrabex 7176 |
. . . . . . . 8
โข (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โ V |
47 | | funmpt 6540 |
. . . . . . . 8
โข Fun
(๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) |
48 | | fvex 6856 |
. . . . . . . 8
โข
(0gโ๐
) โ V |
49 | 46, 47, 48 | 3pm3.2i 1340 |
. . . . . . 7
โข ((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โ V โง Fun (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โง
(0gโ๐
)
โ V) |
50 | 49 | a1i 11 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ท) โ ((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โ V โง Fun (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โง
(0gโ๐
)
โ V)) |
51 | | suppssdm 8109 |
. . . . . . . 8
โข ((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) supp
(0gโ๐
))
โ dom (๐ฅ โ
{๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) |
52 | | eqid 2733 |
. . . . . . . . 9
โข (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) = (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) |
53 | 52 | dmmptss 6194 |
. . . . . . . 8
โข dom
(๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} |
54 | 51, 53 | sstri 3954 |
. . . . . . 7
โข ((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) supp
(0gโ๐
))
โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} |
55 | 54 | a1i 11 |
. . . . . 6
โข ((๐ โง ๐ โ ๐ท) โ ((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) supp
(0gโ๐
))
โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐}) |
56 | | suppssfifsupp 9325 |
. . . . . 6
โข ((((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โ V โง Fun (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) โง
(0gโ๐
)
โ V) โง ({๐ฆ โ
๐ท โฃ ๐ฆ โr โค ๐} โ Fin โง ((๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) supp
(0gโ๐
))
โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐})) โ (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) finSupp
(0gโ๐
)) |
57 | 50, 41, 55, 56 | syl12anc 836 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))) finSupp
(0gโ๐
)) |
58 | 3, 37, 38, 5, 39, 41, 10, 43, 57 | gsummulc2 20036 |
. . . 4
โข ((๐ โง ๐ โ ๐ท) โ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ (๐ด(.rโ๐
)((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))))) = (๐ด(.rโ๐
)(๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))))) |
59 | 36, 58 | eqtrd 2773 |
. . 3
โข ((๐ โง ๐ โ ๐ท) โ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ (((๐ด ยท ๐)โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))) = (๐ด(.rโ๐
)(๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))))) |
60 | 59 | mpteq2dva 5206 |
. 2
โข (๐ โ (๐ โ ๐ท โฆ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ (((๐ด ยท ๐)โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))))) = (๐ โ ๐ท โฆ (๐ด(.rโ๐
)(๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))))))) |
61 | | psrass.t |
. . 3
โข ร =
(.rโ๐) |
62 | 1, 2, 9, 4, 19, 7,
12 | psrvscacl 21377 |
. . 3
โข (๐ โ (๐ด ยท ๐) โ ๐ต) |
63 | 1, 4, 5, 61, 6, 62, 23 | psrmulfval 21369 |
. 2
โข (๐ โ ((๐ด ยท ๐) ร ๐) = (๐ โ ๐ท โฆ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ (((๐ด ยท ๐)โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))))) |
64 | 1, 4, 61, 19, 12, 23 | psrmulcl 21372 |
. . . 4
โข (๐ โ (๐ ร ๐) โ ๐ต) |
65 | 1, 2, 9, 4, 5, 6, 7, 64 | psrvsca 21375 |
. . 3
โข (๐ โ (๐ด ยท (๐ ร ๐)) = ((๐ท ร {๐ด}) โf
(.rโ๐
)(๐ ร ๐))) |
66 | 45 | a1i 11 |
. . . 4
โข (๐ โ ๐ท โ V) |
67 | | ovexd 7393 |
. . . 4
โข ((๐ โง ๐ โ ๐ท) โ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))) โ V) |
68 | | fconstmpt 5695 |
. . . . 5
โข (๐ท ร {๐ด}) = (๐ โ ๐ท โฆ ๐ด) |
69 | 68 | a1i 11 |
. . . 4
โข (๐ โ (๐ท ร {๐ด}) = (๐ โ ๐ท โฆ ๐ด)) |
70 | 1, 4, 5, 61, 6, 12, 23 | psrmulfval 21369 |
. . . 4
โข (๐ โ (๐ ร ๐) = (๐ โ ๐ท โฆ (๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ))))))) |
71 | 66, 8, 67, 69, 70 | offval2 7638 |
. . 3
โข (๐ โ ((๐ท ร {๐ด}) โf
(.rโ๐
)(๐ ร ๐)) = (๐ โ ๐ท โฆ (๐ด(.rโ๐
)(๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))))))) |
72 | 65, 71 | eqtrd 2773 |
. 2
โข (๐ โ (๐ด ยท (๐ ร ๐)) = (๐ โ ๐ท โฆ (๐ด(.rโ๐
)(๐
ฮฃg (๐ฅ โ {๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐} โฆ ((๐โ๐ฅ)(.rโ๐
)(๐โ(๐ โf โ ๐ฅ)))))))) |
73 | 60, 63, 72 | 3eqtr4d 2783 |
1
โข (๐ โ ((๐ด ยท ๐) ร ๐) = (๐ด ยท (๐ ร ๐))) |