Step |
Hyp |
Ref |
Expression |
1 |
|
psrmulcl.s |
โข ๐ = ( ๐ผ mPwSer ๐
) |
2 |
|
psrmulcl.b |
โข ๐ต = ( Base โ ๐ ) |
3 |
|
psrmulcl.t |
โข ยท = ( .r โ ๐ ) |
4 |
|
psrmulcl.r |
โข ( ๐ โ ๐
โ Ring ) |
5 |
|
psrmulcl.x |
โข ( ๐ โ ๐ โ ๐ต ) |
6 |
|
psrmulcl.y |
โข ( ๐ โ ๐ โ ๐ต ) |
7 |
|
psrmulcl.d |
โข ๐ท = { ๐ โ ( โ0 โm ๐ผ ) โฃ ( โก ๐ โ โ ) โ Fin } |
8 |
|
eqid |
โข ( Base โ ๐
) = ( Base โ ๐
) |
9 |
|
eqid |
โข ( 0g โ ๐
) = ( 0g โ ๐
) |
10 |
4
|
adantr |
โข ( ( ๐ โง ๐ โ ๐ท ) โ ๐
โ Ring ) |
11 |
10
|
ringcmnd |
โข ( ( ๐ โง ๐ โ ๐ท ) โ ๐
โ CMnd ) |
12 |
7
|
psrbaglefi |
โข ( ๐ โ ๐ท โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โ Fin ) |
13 |
12
|
adantl |
โข ( ( ๐ โง ๐ โ ๐ท ) โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โ Fin ) |
14 |
|
eqid |
โข ( .r โ ๐
) = ( .r โ ๐
) |
15 |
4
|
ad2antrr |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ๐
โ Ring ) |
16 |
1 8 7 2 5
|
psrelbas |
โข ( ๐ โ ๐ : ๐ท โถ ( Base โ ๐
) ) |
17 |
16
|
ad2antrr |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ๐ : ๐ท โถ ( Base โ ๐
) ) |
18 |
|
simpr |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) |
19 |
|
breq1 |
โข ( ๐ฆ = ๐ฅ โ ( ๐ฆ โr โค ๐ โ ๐ฅ โr โค ๐ ) ) |
20 |
19
|
elrab |
โข ( ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โ ( ๐ฅ โ ๐ท โง ๐ฅ โr โค ๐ ) ) |
21 |
18 20
|
sylib |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ( ๐ฅ โ ๐ท โง ๐ฅ โr โค ๐ ) ) |
22 |
21
|
simpld |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ๐ฅ โ ๐ท ) |
23 |
17 22
|
ffvelcdmd |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ( ๐ โ ๐ฅ ) โ ( Base โ ๐
) ) |
24 |
1 8 7 2 6
|
psrelbas |
โข ( ๐ โ ๐ : ๐ท โถ ( Base โ ๐
) ) |
25 |
24
|
ad2antrr |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ๐ : ๐ท โถ ( Base โ ๐
) ) |
26 |
|
simplr |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ๐ โ ๐ท ) |
27 |
7
|
psrbagf |
โข ( ๐ฅ โ ๐ท โ ๐ฅ : ๐ผ โถ โ0 ) |
28 |
22 27
|
syl |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ๐ฅ : ๐ผ โถ โ0 ) |
29 |
21
|
simprd |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ๐ฅ โr โค ๐ ) |
30 |
7
|
psrbagcon |
โข ( ( ๐ โ ๐ท โง ๐ฅ : ๐ผ โถ โ0 โง ๐ฅ โr โค ๐ ) โ ( ( ๐ โf โ ๐ฅ ) โ ๐ท โง ( ๐ โf โ ๐ฅ ) โr โค ๐ ) ) |
31 |
26 28 29 30
|
syl3anc |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ( ( ๐ โf โ ๐ฅ ) โ ๐ท โง ( ๐ โf โ ๐ฅ ) โr โค ๐ ) ) |
32 |
31
|
simpld |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ( ๐ โf โ ๐ฅ ) โ ๐ท ) |
33 |
25 32
|
ffvelcdmd |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ( ๐ โ ( ๐ โf โ ๐ฅ ) ) โ ( Base โ ๐
) ) |
34 |
8 14 15 23 33
|
ringcld |
โข ( ( ( ๐ โง ๐ โ ๐ท ) โง ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } ) โ ( ( ๐ โ ๐ฅ ) ( .r โ ๐
) ( ๐ โ ( ๐ โf โ ๐ฅ ) ) ) โ ( Base โ ๐
) ) |
35 |
34
|
fmpttd |
โข ( ( ๐ โง ๐ โ ๐ท ) โ ( ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โฆ ( ( ๐ โ ๐ฅ ) ( .r โ ๐
) ( ๐ โ ( ๐ โf โ ๐ฅ ) ) ) ) : { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โถ ( Base โ ๐
) ) |
36 |
|
fvexd |
โข ( ( ๐ โง ๐ โ ๐ท ) โ ( 0g โ ๐
) โ V ) |
37 |
35 13 36
|
fdmfifsupp |
โข ( ( ๐ โง ๐ โ ๐ท ) โ ( ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โฆ ( ( ๐ โ ๐ฅ ) ( .r โ ๐
) ( ๐ โ ( ๐ โf โ ๐ฅ ) ) ) ) finSupp ( 0g โ ๐
) ) |
38 |
8 9 11 13 35 37
|
gsumcl |
โข ( ( ๐ โง ๐ โ ๐ท ) โ ( ๐
ฮฃg ( ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โฆ ( ( ๐ โ ๐ฅ ) ( .r โ ๐
) ( ๐ โ ( ๐ โf โ ๐ฅ ) ) ) ) ) โ ( Base โ ๐
) ) |
39 |
38
|
fmpttd |
โข ( ๐ โ ( ๐ โ ๐ท โฆ ( ๐
ฮฃg ( ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โฆ ( ( ๐ โ ๐ฅ ) ( .r โ ๐
) ( ๐ โ ( ๐ โf โ ๐ฅ ) ) ) ) ) ) : ๐ท โถ ( Base โ ๐
) ) |
40 |
|
fvex |
โข ( Base โ ๐
) โ V |
41 |
|
ovex |
โข ( โ0 โm ๐ผ ) โ V |
42 |
7 41
|
rabex2 |
โข ๐ท โ V |
43 |
40 42
|
elmap |
โข ( ( ๐ โ ๐ท โฆ ( ๐
ฮฃg ( ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โฆ ( ( ๐ โ ๐ฅ ) ( .r โ ๐
) ( ๐ โ ( ๐ โf โ ๐ฅ ) ) ) ) ) ) โ ( ( Base โ ๐
) โm ๐ท ) โ ( ๐ โ ๐ท โฆ ( ๐
ฮฃg ( ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โฆ ( ( ๐ โ ๐ฅ ) ( .r โ ๐
) ( ๐ โ ( ๐ โf โ ๐ฅ ) ) ) ) ) ) : ๐ท โถ ( Base โ ๐
) ) |
44 |
39 43
|
sylibr |
โข ( ๐ โ ( ๐ โ ๐ท โฆ ( ๐
ฮฃg ( ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โฆ ( ( ๐ โ ๐ฅ ) ( .r โ ๐
) ( ๐ โ ( ๐ โf โ ๐ฅ ) ) ) ) ) ) โ ( ( Base โ ๐
) โm ๐ท ) ) |
45 |
1 2 14 3 7 5 6
|
psrmulfval |
โข ( ๐ โ ( ๐ ยท ๐ ) = ( ๐ โ ๐ท โฆ ( ๐
ฮฃg ( ๐ฅ โ { ๐ฆ โ ๐ท โฃ ๐ฆ โr โค ๐ } โฆ ( ( ๐ โ ๐ฅ ) ( .r โ ๐
) ( ๐ โ ( ๐ โf โ ๐ฅ ) ) ) ) ) ) ) |
46 |
|
reldmpsr |
โข Rel dom mPwSer |
47 |
46 1 2
|
elbasov |
โข ( ๐ โ ๐ต โ ( ๐ผ โ V โง ๐
โ V ) ) |
48 |
5 47
|
syl |
โข ( ๐ โ ( ๐ผ โ V โง ๐
โ V ) ) |
49 |
48
|
simpld |
โข ( ๐ โ ๐ผ โ V ) |
50 |
1 8 7 2 49
|
psrbas |
โข ( ๐ โ ๐ต = ( ( Base โ ๐
) โm ๐ท ) ) |
51 |
44 45 50
|
3eltr4d |
โข ( ๐ โ ( ๐ ยท ๐ ) โ ๐ต ) |