Step | Hyp | Ref
| Expression |
1 | | mhpmulcl.y |
. . . . . . . 8
โข ๐ = (๐ผ mPoly ๐
) |
2 | | eqid 2725 |
. . . . . . . 8
โข
(Baseโ๐) =
(Baseโ๐) |
3 | | eqid 2725 |
. . . . . . . 8
โข
(.rโ๐
) = (.rโ๐
) |
4 | | mhpmulcl.t |
. . . . . . . 8
โข ยท =
(.rโ๐) |
5 | | eqid 2725 |
. . . . . . . 8
โข {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} = {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} |
6 | | mhpmulcl.h |
. . . . . . . . 9
โข ๐ป = (๐ผ mHomP ๐
) |
7 | | reldmmhp 22070 |
. . . . . . . . . 10
โข Rel dom
mHomP |
8 | | mhpmulcl.p |
. . . . . . . . . 10
โข (๐ โ ๐ โ (๐ปโ๐)) |
9 | 7, 6, 8 | elfvov1 7458 |
. . . . . . . . 9
โข (๐ โ ๐ผ โ V) |
10 | | mhpmulcl.r |
. . . . . . . . 9
โข (๐ โ ๐
โ Ring) |
11 | | mhpmulcl.m |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ0) |
12 | 6, 1, 2, 9, 10, 11, 8 | mhpmpl 22076 |
. . . . . . . 8
โข (๐ โ ๐ โ (Baseโ๐)) |
13 | | mhpmulcl.n |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ0) |
14 | | mhpmulcl.q |
. . . . . . . . 9
โข (๐ โ ๐ โ (๐ปโ๐)) |
15 | 6, 1, 2, 9, 10, 13, 14 | mhpmpl 22076 |
. . . . . . . 8
โข (๐ โ ๐ โ (Baseโ๐)) |
16 | 1, 2, 3, 4, 5, 12,
15 | mplmul 21960 |
. . . . . . 7
โข (๐ โ (๐ ยท ๐) = (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฆ (๐
ฮฃg
(๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ โf โ ๐))))))) |
17 | 16 | adantr 479 |
. . . . . 6
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ (๐ ยท ๐) = (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฆ (๐
ฮฃg
(๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ โf โ ๐))))))) |
18 | | breq2 5147 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (๐ โr โค ๐ โ ๐ โr โค ๐ฅ)) |
19 | 18 | rabbidv 3427 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐} = {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
20 | | fvoveq1 7439 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (๐โ(๐ โf โ ๐)) = (๐โ(๐ฅ โf โ ๐))) |
21 | 20 | oveq2d 7432 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ ((๐โ๐)(.rโ๐
)(๐โ(๐ โf โ ๐))) = ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐)))) |
22 | 19, 21 | mpteq12dv 5234 |
. . . . . . . 8
โข (๐ = ๐ฅ โ (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ โf โ ๐)))) = (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) |
23 | 22 | oveq2d 7432 |
. . . . . . 7
โข (๐ = ๐ฅ โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ โf โ ๐))))) = (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐)))))) |
24 | 23 | adantl 480 |
. . . . . 6
โข (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง ๐ = ๐ฅ) โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ โf โ ๐))))) = (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐)))))) |
25 | | simpr 483 |
. . . . . 6
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
26 | | ovexd 7451 |
. . . . . 6
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ (๐
ฮฃg
(๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) โ V) |
27 | 17, 24, 25, 26 | fvmptd 7007 |
. . . . 5
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ ((๐ ยท ๐)โ๐ฅ) = (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐)))))) |
28 | 27 | neeq1d 2990 |
. . . 4
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ (((๐ ยท ๐)โ๐ฅ) โ (0gโ๐
) โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) โ
(0gโ๐
))) |
29 | | simp-4l 781 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐) |
30 | | oveq2 7424 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ ((โfld
โพs โ0) ฮฃg ๐) = ((โfld
โพs โ0) ฮฃg ๐)) |
31 | 30 | eqeq1d 2727 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (((โfld
โพs โ0) ฮฃg ๐) = ๐ โ ((โfld
โพs โ0) ฮฃg ๐) = ๐)) |
32 | 31 | necon3bbid 2968 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (ยฌ ((โfld
โพs โ0) ฮฃg ๐) = ๐ โ ((โfld
โพs โ0) ฮฃg ๐) โ ๐)) |
33 | | simplr 767 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
34 | | elrabi 3668 |
. . . . . . . . . . . . . . . 16
โข (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โ ๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
36 | | simpr 483 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ((โfld
โพs โ0) ฮฃg ๐) โ ๐) |
37 | 32, 35, 36 | elrabd 3676 |
. . . . . . . . . . . . . 14
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ยฌ
((โfld โพs โ0)
ฮฃg ๐) = ๐}) |
38 | | notrab 4307 |
. . . . . . . . . . . . . 14
โข ({โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐}) = {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ยฌ
((โfld โพs โ0)
ฮฃg ๐) = ๐} |
39 | 37, 38 | eleqtrrdi 2836 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐ โ ({โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐})) |
40 | | eqid 2725 |
. . . . . . . . . . . . . . 15
โข
(Baseโ๐
) =
(Baseโ๐
) |
41 | 1, 40, 2, 5, 12 | mplelf 21947 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐:{โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}โถ(Baseโ๐
)) |
42 | | eqid 2725 |
. . . . . . . . . . . . . . 15
โข
(0gโ๐
) = (0gโ๐
) |
43 | 6, 42, 5, 9, 10, 11, 8 | mhpdeg 22077 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ supp (0gโ๐
)) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐}) |
44 | | ovex 7449 |
. . . . . . . . . . . . . . . 16
โข
(โ0 โm ๐ผ) โ V |
45 | 44 | rabex 5329 |
. . . . . . . . . . . . . . 15
โข {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ
V |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ
V) |
47 | | fvexd 6907 |
. . . . . . . . . . . . . 14
โข (๐ โ (0gโ๐
) โ V) |
48 | 41, 43, 46, 47 | suppssr 8199 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ({โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐})) โ (๐โ๐) = (0gโ๐
)) |
49 | 29, 39, 48 | syl2anc 582 |
. . . . . . . . . . . 12
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ (๐โ๐) = (0gโ๐
)) |
50 | 49 | oveq1d 7431 |
. . . . . . . . . . 11
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) =
((0gโ๐
)(.rโ๐
)(๐โ(๐ฅ โf โ ๐)))) |
51 | 10 | ad4antr 730 |
. . . . . . . . . . . 12
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐
โ Ring) |
52 | 15 | ad4antr 730 |
. . . . . . . . . . . . . 14
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐ โ (Baseโ๐)) |
53 | 1, 40, 2, 5, 52 | mplelf 21947 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐:{โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}โถ(Baseโ๐
)) |
54 | | simp-4r 782 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
55 | | eqid 2725 |
. . . . . . . . . . . . . . . 16
โข {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} = {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} |
56 | 5, 55 | psrbagconcl 21871 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ฅ โf โ ๐) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
57 | 54, 33, 56 | syl2anc 582 |
. . . . . . . . . . . . . 14
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ (๐ฅ โf โ ๐) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
58 | | elrabi 3668 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โf โ
๐) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โ (๐ฅ โf โ ๐) โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
59 | 57, 58 | syl 17 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ (๐ฅ โf โ ๐) โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
60 | 53, 59 | ffvelcdmd 7090 |
. . . . . . . . . . . 12
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ (๐โ(๐ฅ โf โ ๐)) โ (Baseโ๐
)) |
61 | 40, 3, 42 | ringlz 20233 |
. . . . . . . . . . . 12
โข ((๐
โ Ring โง (๐โ(๐ฅ โf โ ๐)) โ (Baseโ๐
)) โ
((0gโ๐
)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) = (0gโ๐
)) |
62 | 51, 60, 61 | syl2anc 582 |
. . . . . . . . . . 11
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ((0gโ๐
)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) = (0gโ๐
)) |
63 | 50, 62 | eqtrd 2765 |
. . . . . . . . . 10
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) = (0gโ๐
)) |
64 | | simp-4l 781 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐) |
65 | | oveq2 7424 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ฅ โf โ ๐) โ ((โfld
โพs โ0) ฮฃg ๐) = ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐))) |
66 | 65 | eqeq1d 2727 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ฅ โf โ ๐) โ
(((โfld โพs โ0)
ฮฃg ๐) = ๐ โ ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) = ๐)) |
67 | 66 | necon3bbid 2968 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ฅ โf โ ๐) โ (ยฌ
((โfld โพs โ0)
ฮฃg ๐) = ๐ โ ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐)) |
68 | | simp-4r 782 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
69 | | simplr 767 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
70 | 68, 69, 56 | syl2anc 582 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ (๐ฅ โf โ ๐) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
71 | 70, 58 | syl 17 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ (๐ฅ โf โ ๐) โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
72 | | simpr 483 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) |
73 | 67, 71, 72 | elrabd 3676 |
. . . . . . . . . . . . . 14
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ (๐ฅ โf โ ๐) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ยฌ
((โfld โพs โ0)
ฮฃg ๐) = ๐}) |
74 | | notrab 4307 |
. . . . . . . . . . . . . 14
โข ({โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐}) = {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ยฌ
((โfld โพs โ0)
ฮฃg ๐) = ๐} |
75 | 73, 74 | eleqtrrdi 2836 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ (๐ฅ โf โ ๐) โ ({โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐})) |
76 | 1, 40, 2, 5, 15 | mplelf 21947 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐:{โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}โถ(Baseโ๐
)) |
77 | 6, 42, 5, 9, 10, 13, 14 | mhpdeg 22077 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ supp (0gโ๐
)) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐}) |
78 | 76, 77, 46, 47 | suppssr 8199 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โf โ ๐) โ ({โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐})) โ (๐โ(๐ฅ โf โ ๐)) = (0gโ๐
)) |
79 | 64, 75, 78 | syl2anc 582 |
. . . . . . . . . . . 12
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ (๐โ(๐ฅ โf โ ๐)) = (0gโ๐
)) |
80 | 79 | oveq2d 7432 |
. . . . . . . . . . 11
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) = ((๐โ๐)(.rโ๐
)(0gโ๐
))) |
81 | 10 | ad4antr 730 |
. . . . . . . . . . . 12
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐
โ Ring) |
82 | 12 | ad4antr 730 |
. . . . . . . . . . . . . 14
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐ โ (Baseโ๐)) |
83 | 1, 40, 2, 5, 82 | mplelf 21947 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐:{โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}โถ(Baseโ๐
)) |
84 | 34 | adantl 480 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
85 | 84 | adantr 479 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
86 | 83, 85 | ffvelcdmd 7090 |
. . . . . . . . . . . 12
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ (๐โ๐) โ (Baseโ๐
)) |
87 | 40, 3, 42 | ringrz 20234 |
. . . . . . . . . . . 12
โข ((๐
โ Ring โง (๐โ๐) โ (Baseโ๐
)) โ ((๐โ๐)(.rโ๐
)(0gโ๐
)) = (0gโ๐
)) |
88 | 81, 86, 87 | syl2anc 582 |
. . . . . . . . . . 11
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ((๐โ๐)(.rโ๐
)(0gโ๐
)) = (0gโ๐
)) |
89 | 80, 88 | eqtrd 2765 |
. . . . . . . . . 10
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) = (0gโ๐
)) |
90 | | nn0subm 21359 |
. . . . . . . . . . . . . . . 16
โข
โ0 โ
(SubMndโโfld) |
91 | | eqid 2725 |
. . . . . . . . . . . . . . . . 17
โข
(โfld โพs โ0) =
(โfld โพs
โ0) |
92 | 91 | submbas 18770 |
. . . . . . . . . . . . . . . 16
โข
(โ0 โ (SubMndโโfld) โ
โ0 = (Baseโ(โfld โพs
โ0))) |
93 | 90, 92 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข
โ0 = (Baseโ(โfld
โพs โ0)) |
94 | | cnfld0 21324 |
. . . . . . . . . . . . . . . . 17
โข 0 =
(0gโโfld) |
95 | 91, 94 | subm0 18771 |
. . . . . . . . . . . . . . . 16
โข
(โ0 โ (SubMndโโfld) โ
0 = (0gโ(โfld โพs
โ0))) |
96 | 90, 95 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข 0 =
(0gโ(โfld โพs
โ0)) |
97 | | nn0ex 12508 |
. . . . . . . . . . . . . . . 16
โข
โ0 โ V |
98 | | cnfldadd 21289 |
. . . . . . . . . . . . . . . . 17
โข + =
(+gโโfld) |
99 | 91, 98 | ressplusg 17270 |
. . . . . . . . . . . . . . . 16
โข
(โ0 โ V โ + =
(+gโ(โfld โพs
โ0))) |
100 | 97, 99 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข + =
(+gโ(โfld โพs
โ0)) |
101 | | cnring 21322 |
. . . . . . . . . . . . . . . . . 18
โข
โfld โ Ring |
102 | | ringcmn 20222 |
. . . . . . . . . . . . . . . . . 18
โข
(โfld โ Ring โ โfld โ
CMnd) |
103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
โข
โfld โ CMnd |
104 | 91 | submcmn 19797 |
. . . . . . . . . . . . . . . . 17
โข
((โfld โ CMnd โง โ0 โ
(SubMndโโfld)) โ (โfld
โพs โ0) โ CMnd) |
105 | 103, 90, 104 | mp2an 690 |
. . . . . . . . . . . . . . . 16
โข
(โfld โพs โ0) โ
CMnd |
106 | 105 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (โfld
โพs โ0) โ CMnd) |
107 | 9 | ad3antrrr 728 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ผ โ V) |
108 | 5 | psrbagf 21855 |
. . . . . . . . . . . . . . . 16
โข (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ ๐:๐ผโถโ0) |
109 | 84, 108 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐:๐ผโถโ0) |
110 | | simpllr 774 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
111 | 5 | psrbagf 21855 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ ๐ฅ:๐ผโถโ0) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ฅ:๐ผโถโ0) |
113 | 112 | ffnd 6718 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ฅ Fn ๐ผ) |
114 | 109 | ffnd 6718 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ Fn ๐ผ) |
115 | | inidm 4213 |
. . . . . . . . . . . . . . . . 17
โข (๐ผ โฉ ๐ผ) = ๐ผ |
116 | | eqidd 2726 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐ฅโ๐) = (๐ฅโ๐)) |
117 | | eqidd 2726 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐โ๐) = (๐โ๐)) |
118 | 113, 114,
107, 107, 115, 116, 117 | offval 7691 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ฅ โf โ ๐) = (๐ โ ๐ผ โฆ ((๐ฅโ๐) โ (๐โ๐)))) |
119 | | simpl 481 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ})) |
120 | | simplr 767 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
121 | | breq1 5146 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ (๐ โr โค ๐ฅ โ ๐ โr โค ๐ฅ)) |
122 | 121 | elrab 3674 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โ (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โง ๐ โr โค ๐ฅ)) |
123 | 122 | simprbi 495 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โ ๐ โr โค ๐ฅ) |
124 | 120, 123 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ๐ โr โค ๐ฅ) |
125 | | simpr 483 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ๐ โ ๐ผ) |
126 | 114, 113,
107, 107, 115, 117, 116 | ofrval 7694 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โr โค ๐ฅ โง ๐ โ ๐ผ) โ (๐โ๐) โค (๐ฅโ๐)) |
127 | 119, 124,
125, 126 | syl3anc 1368 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐โ๐) โค (๐ฅโ๐)) |
128 | 109 | ffvelcdmda 7089 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐โ๐) โ
โ0) |
129 | 112 | ffvelcdmda 7089 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐ฅโ๐) โ
โ0) |
130 | | nn0sub 12552 |
. . . . . . . . . . . . . . . . . 18
โข (((๐โ๐) โ โ0 โง (๐ฅโ๐) โ โ0) โ ((๐โ๐) โค (๐ฅโ๐) โ ((๐ฅโ๐) โ (๐โ๐)) โ
โ0)) |
131 | 128, 129,
130 | syl2anc 582 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ((๐โ๐) โค (๐ฅโ๐) โ ((๐ฅโ๐) โ (๐โ๐)) โ
โ0)) |
132 | 127, 131 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ((๐ฅโ๐) โ (๐โ๐)) โ
โ0) |
133 | 118, 132 | fmpt3d 7121 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ฅ โf โ ๐):๐ผโถโ0) |
134 | 109 | ffund 6721 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ Fun ๐) |
135 | | c0ex 11238 |
. . . . . . . . . . . . . . . . . . . 20
โข 0 โ
V |
136 | 107, 135 | jctir 519 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ผ โ V โง 0 โ
V)) |
137 | | fsuppeq 8178 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ผ โ V โง 0 โ V)
โ (๐:๐ผโถโ0 โ (๐ supp 0) = (โก๐ โ (โ0 โ
{0})))) |
138 | 136, 109,
137 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ supp 0) = (โก๐ โ (โ0 โ
{0}))) |
139 | | dfn2 12515 |
. . . . . . . . . . . . . . . . . . 19
โข โ =
(โ0 โ {0}) |
140 | 139 | imaeq2i 6056 |
. . . . . . . . . . . . . . . . . 18
โข (โก๐ โ โ) = (โก๐ โ (โ0 โ
{0})) |
141 | 138, 140 | eqtr4di 2783 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ supp 0) = (โก๐ โ โ)) |
142 | 5 | psrbag 21854 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ผ โ V โ (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ (๐:๐ผโถโ0 โง (โก๐ โ โ) โ
Fin))) |
143 | 107, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ (๐:๐ผโถโ0 โง (โก๐ โ โ) โ
Fin))) |
144 | 84, 143 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐:๐ผโถโ0 โง (โก๐ โ โ) โ
Fin)) |
145 | 144 | simprd 494 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (โก๐ โ โ) โ
Fin) |
146 | 141, 145 | eqeltrd 2825 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ supp 0) โ Fin) |
147 | 84 | elexd 3484 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ โ V) |
148 | | isfsupp 9389 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ V โง 0 โ V)
โ (๐ finSupp 0 โ
(Fun ๐ โง (๐ supp 0) โ
Fin))) |
149 | 147, 135,
148 | sylancl 584 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ finSupp 0 โ (Fun ๐ โง (๐ supp 0) โ Fin))) |
150 | 134, 146,
149 | mpbir2and 711 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ finSupp 0) |
151 | 113, 114,
107, 107 | offun 7696 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ Fun (๐ฅ โf โ
๐)) |
152 | 5 | psrbagfsupp 21857 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ ๐ฅ finSupp 0) |
153 | 110, 152 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ฅ finSupp 0) |
154 | 153, 150 | fsuppunfi 9411 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ((๐ฅ supp 0) โช (๐ supp 0)) โ Fin) |
155 | | 0nn0 12517 |
. . . . . . . . . . . . . . . . . . 19
โข 0 โ
โ0 |
156 | 155 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ 0 โ
โ0) |
157 | | 0m0e0 12362 |
. . . . . . . . . . . . . . . . . . 19
โข (0
โ 0) = 0 |
158 | 157 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (0 โ 0) =
0) |
159 | 107, 156,
112, 109, 158 | suppofssd 8207 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ((๐ฅ โf โ ๐) supp 0) โ ((๐ฅ supp 0) โช (๐ supp 0))) |
160 | 154, 159 | ssfid 9290 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ((๐ฅ โf โ ๐) supp 0) โ
Fin) |
161 | | ovexd 7451 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ฅ โf โ ๐) โ V) |
162 | | isfsupp 9389 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฅ โf โ
๐) โ V โง 0 โ
V) โ ((๐ฅ
โf โ ๐) finSupp 0 โ (Fun (๐ฅ โf โ ๐) โง ((๐ฅ โf โ ๐) supp 0) โ
Fin))) |
163 | 161, 135,
162 | sylancl 584 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ((๐ฅ โf โ ๐) finSupp 0 โ (Fun (๐ฅ โf โ
๐) โง ((๐ฅ โf โ
๐) supp 0) โ
Fin))) |
164 | 151, 160,
163 | mpbir2and 711 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ฅ โf โ ๐) finSupp 0) |
165 | 93, 96, 100, 106, 107, 109, 133, 150, 164 | gsumadd 19882 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ
((โfld โพs โ0)
ฮฃg (๐ โf + (๐ฅ โf โ ๐))) = (((โfld
โพs โ0) ฮฃg ๐) + ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)))) |
166 | 109 | ffvelcdmda 7089 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐โ๐) โ
โ0) |
167 | 166 | nn0cnd 12564 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐โ๐) โ โ) |
168 | 112 | ffvelcdmda 7089 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐ฅโ๐) โ
โ0) |
169 | 168 | nn0cnd 12564 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐ฅโ๐) โ โ) |
170 | 167, 169 | pncan3d 11604 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ((๐โ๐) + ((๐ฅโ๐) โ (๐โ๐))) = (๐ฅโ๐)) |
171 | 170 | mpteq2dva 5243 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ โ ๐ผ โฆ ((๐โ๐) + ((๐ฅโ๐) โ (๐โ๐)))) = (๐ โ ๐ผ โฆ (๐ฅโ๐))) |
172 | | fvexd 6907 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐โ๐) โ V) |
173 | | ovexd 7451 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ((๐ฅโ๐) โ (๐โ๐)) โ V) |
174 | 109 | feqmptd 6962 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ = (๐ โ ๐ผ โฆ (๐โ๐))) |
175 | 112 | feqmptd 6962 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ฅ = (๐ โ ๐ผ โฆ (๐ฅโ๐))) |
176 | 107, 168,
166, 175, 174 | offval2 7702 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ฅ โf โ ๐) = (๐ โ ๐ผ โฆ ((๐ฅโ๐) โ (๐โ๐)))) |
177 | 107, 172,
173, 174, 176 | offval2 7702 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ โf + (๐ฅ โf โ ๐)) = (๐ โ ๐ผ โฆ ((๐โ๐) + ((๐ฅโ๐) โ (๐โ๐))))) |
178 | 171, 177,
175 | 3eqtr4d 2775 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ โf + (๐ฅ โf โ ๐)) = ๐ฅ) |
179 | 178 | oveq2d 7432 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ
((โfld โพs โ0)
ฮฃg (๐ โf + (๐ฅ โf โ ๐))) = ((โfld
โพs โ0) ฮฃg ๐ฅ)) |
180 | 165, 179 | eqtr3d 2767 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ
(((โfld โพs โ0)
ฮฃg ๐) + ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐))) =
((โfld โพs โ0)
ฮฃg ๐ฅ)) |
181 | | simplr 767 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) |
182 | 180, 181 | eqnetrd 2998 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ
(((โfld โพs โ0)
ฮฃg ๐) + ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐))) โ (๐ + ๐)) |
183 | | oveq12 7425 |
. . . . . . . . . . . . . 14
โข
((((โfld โพs โ0)
ฮฃg ๐) = ๐ โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) = ๐) โ (((โfld
โพs โ0) ฮฃg ๐) + ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐))) = (๐ + ๐)) |
184 | 183 | a1i 11 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ
((((โfld โพs โ0)
ฮฃg ๐) = ๐ โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) = ๐) โ (((โfld
โพs โ0) ฮฃg ๐) + ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐))) = (๐ + ๐))) |
185 | 184 | necon3ad 2943 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ
((((โfld โพs โ0)
ฮฃg ๐) + ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐))) โ (๐ + ๐) โ ยฌ (((โfld
โพs โ0) ฮฃg ๐) = ๐ โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) = ๐))) |
186 | 182, 185 | mpd 15 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ยฌ
(((โfld โพs โ0)
ฮฃg ๐) = ๐ โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) = ๐)) |
187 | | neorian 3027 |
. . . . . . . . . . 11
โข
((((โfld โพs โ0)
ฮฃg ๐) โ ๐ โจ ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ยฌ (((โfld
โพs โ0) ฮฃg ๐) = ๐ โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) = ๐)) |
188 | 186, 187 | sylibr 233 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ
(((โfld โพs โ0)
ฮฃg ๐) โ ๐ โจ ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐)) |
189 | 63, 89, 188 | mpjaodan 956 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) = (0gโ๐
)) |
190 | 189 | mpteq2dva 5243 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โ (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐)))) = (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ
(0gโ๐
))) |
191 | 190 | oveq2d 7432 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) = (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ
(0gโ๐
)))) |
192 | | ringmnd 20187 |
. . . . . . . . . 10
โข (๐
โ Ring โ ๐
โ Mnd) |
193 | 10, 192 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐
โ Mnd) |
194 | 193 | ad2antrr 724 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โ ๐
โ Mnd) |
195 | 45 | rabex 5329 |
. . . . . . . 8
โข {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โ V |
196 | 42 | gsumz 18792 |
. . . . . . . 8
โข ((๐
โ Mnd โง {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โ V) โ (๐
ฮฃg
(๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ
(0gโ๐
))) =
(0gโ๐
)) |
197 | 194, 195,
196 | sylancl 584 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ
(0gโ๐
))) =
(0gโ๐
)) |
198 | 191, 197 | eqtrd 2765 |
. . . . . 6
โข (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) =
(0gโ๐
)) |
199 | 198 | ex 411 |
. . . . 5
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ
(((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐) โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) =
(0gโ๐
))) |
200 | 199 | necon1d 2952 |
. . . 4
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ ((๐
ฮฃg
(๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) โ
(0gโ๐
)
โ ((โfld โพs โ0)
ฮฃg ๐ฅ) = (๐ + ๐))) |
201 | 28, 200 | sylbid 239 |
. . 3
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ (((๐ ยท ๐)โ๐ฅ) โ (0gโ๐
) โ ((โfld
โพs โ0) ฮฃg ๐ฅ) = (๐ + ๐))) |
202 | 201 | ralrimiva 3136 |
. 2
โข (๐ โ โ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} (((๐ ยท ๐)โ๐ฅ) โ (0gโ๐
) โ ((โfld
โพs โ0) ฮฃg ๐ฅ) = (๐ + ๐))) |
203 | 11, 13 | nn0addcld 12566 |
. . 3
โข (๐ โ (๐ + ๐) โ
โ0) |
204 | 1 | mplring 21968 |
. . . . 5
โข ((๐ผ โ V โง ๐
โ Ring) โ ๐ โ Ring) |
205 | 9, 10, 204 | syl2anc 582 |
. . . 4
โข (๐ โ ๐ โ Ring) |
206 | 2, 4 | ringcl 20194 |
. . . 4
โข ((๐ โ Ring โง ๐ โ (Baseโ๐) โง ๐ โ (Baseโ๐)) โ (๐ ยท ๐) โ (Baseโ๐)) |
207 | 205, 12, 15, 206 | syl3anc 1368 |
. . 3
โข (๐ โ (๐ ยท ๐) โ (Baseโ๐)) |
208 | 6, 1, 2, 42, 5, 9,
10, 203, 207 | ismhp3 22075 |
. 2
โข (๐ โ ((๐ ยท ๐) โ (๐ปโ(๐ + ๐)) โ โ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} (((๐ ยท ๐)โ๐ฅ) โ (0gโ๐
) โ ((โfld
โพs โ0) ฮฃg ๐ฅ) = (๐ + ๐)))) |
209 | 202, 208 | mpbird 256 |
1
โข (๐ โ (๐ ยท ๐) โ (๐ปโ(๐ + ๐))) |