Step | Hyp | Ref
| Expression |
1 | | mhpmulcl.y |
. . . . . . . 8
โข ๐ = (๐ผ mPoly ๐
) |
2 | | eqid 2737 |
. . . . . . . 8
โข
(Baseโ๐) =
(Baseโ๐) |
3 | | eqid 2737 |
. . . . . . . 8
โข
(.rโ๐
) = (.rโ๐
) |
4 | | mhpmulcl.t |
. . . . . . . 8
โข ยท =
(.rโ๐) |
5 | | eqid 2737 |
. . . . . . . 8
โข {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} = {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} |
6 | | mhpmulcl.h |
. . . . . . . . 9
โข ๐ป = (๐ผ mHomP ๐
) |
7 | | mhpmulcl.i |
. . . . . . . . 9
โข (๐ โ ๐ผ โ ๐) |
8 | | mhpmulcl.r |
. . . . . . . . 9
โข (๐ โ ๐
โ Ring) |
9 | | mhpmulcl.m |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ0) |
10 | | mhpmulcl.p |
. . . . . . . . 9
โข (๐ โ ๐ โ (๐ปโ๐)) |
11 | 6, 1, 2, 7, 8, 9, 10 | mhpmpl 21550 |
. . . . . . . 8
โข (๐ โ ๐ โ (Baseโ๐)) |
12 | | mhpmulcl.n |
. . . . . . . . 9
โข (๐ โ ๐ โ
โ0) |
13 | | mhpmulcl.q |
. . . . . . . . 9
โข (๐ โ ๐ โ (๐ปโ๐)) |
14 | 6, 1, 2, 7, 8, 12,
13 | mhpmpl 21550 |
. . . . . . . 8
โข (๐ โ ๐ โ (Baseโ๐)) |
15 | 1, 2, 3, 4, 5, 11,
14 | mplmul 21431 |
. . . . . . 7
โข (๐ โ (๐ ยท ๐) = (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฆ (๐
ฮฃg
(๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ โf โ ๐))))))) |
16 | 15 | adantr 482 |
. . . . . 6
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ (๐ ยท ๐) = (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฆ (๐
ฮฃg
(๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ โf โ ๐))))))) |
17 | | breq2 5114 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (๐ โr โค ๐ โ ๐ โr โค ๐ฅ)) |
18 | 17 | rabbidv 3418 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐} = {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
19 | | fvoveq1 7385 |
. . . . . . . . . 10
โข (๐ = ๐ฅ โ (๐โ(๐ โf โ ๐)) = (๐โ(๐ฅ โf โ ๐))) |
20 | 19 | oveq2d 7378 |
. . . . . . . . 9
โข (๐ = ๐ฅ โ ((๐โ๐)(.rโ๐
)(๐โ(๐ โf โ ๐))) = ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐)))) |
21 | 18, 20 | mpteq12dv 5201 |
. . . . . . . 8
โข (๐ = ๐ฅ โ (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ โf โ ๐)))) = (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) |
22 | 21 | oveq2d 7378 |
. . . . . . 7
โข (๐ = ๐ฅ โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ โf โ ๐))))) = (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐)))))) |
23 | 22 | adantl 483 |
. . . . . 6
โข (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง ๐ = ๐ฅ) โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ โf โ ๐))))) = (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐)))))) |
24 | | simpr 486 |
. . . . . 6
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
25 | | ovexd 7397 |
. . . . . 6
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ (๐
ฮฃg
(๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) โ V) |
26 | 16, 23, 24, 25 | fvmptd 6960 |
. . . . 5
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ ((๐ ยท ๐)โ๐ฅ) = (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐)))))) |
27 | 26 | neeq1d 3004 |
. . . 4
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ (((๐ ยท ๐)โ๐ฅ) โ (0gโ๐
) โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) โ
(0gโ๐
))) |
28 | | simp-4l 782 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐) |
29 | | oveq2 7370 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ ((โfld
โพs โ0) ฮฃg ๐) = ((โfld
โพs โ0) ฮฃg ๐)) |
30 | 29 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (((โfld
โพs โ0) ฮฃg ๐) = ๐ โ ((โfld
โพs โ0) ฮฃg ๐) = ๐)) |
31 | 30 | necon3bbid 2982 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (ยฌ ((โfld
โพs โ0) ฮฃg ๐) = ๐ โ ((โfld
โพs โ0) ฮฃg ๐) โ ๐)) |
32 | | simplr 768 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
33 | | elrabi 3644 |
. . . . . . . . . . . . . . . 16
โข (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โ ๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
35 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ((โfld
โพs โ0) ฮฃg ๐) โ ๐) |
36 | 31, 34, 35 | elrabd 3652 |
. . . . . . . . . . . . . 14
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ยฌ
((โfld โพs โ0)
ฮฃg ๐) = ๐}) |
37 | | notrab 4276 |
. . . . . . . . . . . . . 14
โข ({โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐}) = {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ยฌ
((โfld โพs โ0)
ฮฃg ๐) = ๐} |
38 | 36, 37 | eleqtrrdi 2849 |
. . . . . . . . . . . . 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 ๐) = ๐})) |
39 | | eqid 2737 |
. . . . . . . . . . . . . . 15
โข
(Baseโ๐
) =
(Baseโ๐
) |
40 | 1, 39, 2, 5, 11 | mplelf 21420 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐:{โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}โถ(Baseโ๐
)) |
41 | | eqid 2737 |
. . . . . . . . . . . . . . 15
โข
(0gโ๐
) = (0gโ๐
) |
42 | 6, 41, 5, 7, 8, 9, 10 | mhpdeg 21551 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ supp (0gโ๐
)) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐}) |
43 | | ovex 7395 |
. . . . . . . . . . . . . . . 16
โข
(โ0 โm ๐ผ) โ V |
44 | 43 | rabex 5294 |
. . . . . . . . . . . . . . 15
โข {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ
V |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ
V) |
46 | | fvexd 6862 |
. . . . . . . . . . . . . 14
โข (๐ โ (0gโ๐
) โ V) |
47 | 40, 42, 45, 46 | suppssr 8132 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ({โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐})) โ (๐โ๐) = (0gโ๐
)) |
48 | 28, 38, 47 | syl2anc 585 |
. . . . . . . . . . . 12
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ (๐โ๐) = (0gโ๐
)) |
49 | 48 | oveq1d 7377 |
. . . . . . . . . . 11
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) =
((0gโ๐
)(.rโ๐
)(๐โ(๐ฅ โf โ ๐)))) |
50 | 8 | ad4antr 731 |
. . . . . . . . . . . 12
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐
โ Ring) |
51 | 14 | ad4antr 731 |
. . . . . . . . . . . . . 14
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐ โ (Baseโ๐)) |
52 | 1, 39, 2, 5, 51 | mplelf 21420 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐:{โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}โถ(Baseโ๐
)) |
53 | | simp-4r 783 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
54 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
โข {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} = {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} |
55 | 5, 54 | psrbagconcl 21352 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ฅ โf โ ๐) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
56 | 53, 32, 55 | syl2anc 585 |
. . . . . . . . . . . . . 14
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ (๐ฅ โf โ ๐) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
57 | | elrabi 3644 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โf โ
๐) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โ (๐ฅ โf โ ๐) โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ (๐ฅ โf โ ๐) โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
59 | 52, 58 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ (๐โ(๐ฅ โf โ ๐)) โ (Baseโ๐
)) |
60 | 39, 3, 41 | ringlz 20018 |
. . . . . . . . . . . 12
โข ((๐
โ Ring โง (๐โ(๐ฅ โf โ ๐)) โ (Baseโ๐
)) โ
((0gโ๐
)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) = (0gโ๐
)) |
61 | 50, 59, 60 | syl2anc 585 |
. . . . . . . . . . 11
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ((0gโ๐
)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) = (0gโ๐
)) |
62 | 49, 61 | eqtrd 2777 |
. . . . . . . . . 10
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg ๐) โ ๐) โ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) = (0gโ๐
)) |
63 | | simp-4l 782 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐) |
64 | | oveq2 7370 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ฅ โf โ ๐) โ ((โfld
โพs โ0) ฮฃg ๐) = ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐))) |
65 | 64 | eqeq1d 2739 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ฅ โf โ ๐) โ
(((โfld โพs โ0)
ฮฃg ๐) = ๐ โ ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) = ๐)) |
66 | 65 | necon3bbid 2982 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ฅ โf โ ๐) โ (ยฌ
((โfld โพs โ0)
ฮฃg ๐) = ๐ โ ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐)) |
67 | | simp-4r 783 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
68 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
69 | 67, 68, 55 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ (๐ฅ โf โ ๐) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
70 | 69, 57 | syl 17 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ (๐ฅ โf โ ๐) โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
71 | | simpr 486 |
. . . . . . . . . . . . . . 15
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) |
72 | 66, 70, 71 | elrabd 3652 |
. . . . . . . . . . . . . 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 ๐) = ๐}) |
73 | | notrab 4276 |
. . . . . . . . . . . . . 14
โข ({โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐}) = {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ยฌ
((โfld โพs โ0)
ฮฃg ๐) = ๐} |
74 | 72, 73 | eleqtrrdi 2849 |
. . . . . . . . . . . . 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 ๐) = ๐})) |
75 | 1, 39, 2, 5, 14 | mplelf 21420 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐:{โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}โถ(Baseโ๐
)) |
76 | 6, 41, 5, 7, 8, 12,
13 | mhpdeg 21551 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ supp (0gโ๐
)) โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐}) |
77 | 75, 76, 45, 46 | suppssr 8132 |
. . . . . . . . . . . . 13
โข ((๐ โง (๐ฅ โf โ ๐) โ ({โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ
((โfld โพs โ0)
ฮฃg ๐) = ๐})) โ (๐โ(๐ฅ โf โ ๐)) = (0gโ๐
)) |
78 | 63, 74, 77 | syl2anc 585 |
. . . . . . . . . . . 12
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ (๐โ(๐ฅ โf โ ๐)) = (0gโ๐
)) |
79 | 78 | oveq2d 7378 |
. . . . . . . . . . 11
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) = ((๐โ๐)(.rโ๐
)(0gโ๐
))) |
80 | 8 | ad4antr 731 |
. . . . . . . . . . . 12
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐
โ Ring) |
81 | 11 | ad4antr 731 |
. . . . . . . . . . . . . 14
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐ โ (Baseโ๐)) |
82 | 1, 39, 2, 5, 81 | mplelf 21420 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐:{โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}โถ(Baseโ๐
)) |
83 | 33 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
84 | 83 | adantr 482 |
. . . . . . . . . . . . 13
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
85 | 82, 84 | ffvelcdmd 7041 |
. . . . . . . . . . . 12
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ (๐โ๐) โ (Baseโ๐
)) |
86 | 39, 3, 41 | ringrz 20019 |
. . . . . . . . . . . 12
โข ((๐
โ Ring โง (๐โ๐) โ (Baseโ๐
)) โ ((๐โ๐)(.rโ๐
)(0gโ๐
)) = (0gโ๐
)) |
87 | 80, 85, 86 | syl2anc 585 |
. . . . . . . . . . 11
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ((๐โ๐)(.rโ๐
)(0gโ๐
)) = (0gโ๐
)) |
88 | 79, 87 | eqtrd 2777 |
. . . . . . . . . 10
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) = (0gโ๐
)) |
89 | | nn0subm 20868 |
. . . . . . . . . . . . . . . 16
โข
โ0 โ
(SubMndโโfld) |
90 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
โข
(โfld โพs โ0) =
(โfld โพs
โ0) |
91 | 90 | submbas 18632 |
. . . . . . . . . . . . . . . 16
โข
(โ0 โ (SubMndโโfld) โ
โ0 = (Baseโ(โfld โพs
โ0))) |
92 | 89, 91 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข
โ0 = (Baseโ(โfld
โพs โ0)) |
93 | | cnfld0 20837 |
. . . . . . . . . . . . . . . . 17
โข 0 =
(0gโโfld) |
94 | 90, 93 | subm0 18633 |
. . . . . . . . . . . . . . . 16
โข
(โ0 โ (SubMndโโfld) โ
0 = (0gโ(โfld โพs
โ0))) |
95 | 89, 94 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข 0 =
(0gโ(โfld โพs
โ0)) |
96 | | nn0ex 12426 |
. . . . . . . . . . . . . . . 16
โข
โ0 โ V |
97 | | cnfldadd 20817 |
. . . . . . . . . . . . . . . . 17
โข + =
(+gโโfld) |
98 | 90, 97 | ressplusg 17178 |
. . . . . . . . . . . . . . . 16
โข
(โ0 โ V โ + =
(+gโ(โfld โพs
โ0))) |
99 | 96, 98 | ax-mp 5 |
. . . . . . . . . . . . . . 15
โข + =
(+gโ(โfld โพs
โ0)) |
100 | | cnring 20835 |
. . . . . . . . . . . . . . . . . 18
โข
โfld โ Ring |
101 | | ringcmn 20010 |
. . . . . . . . . . . . . . . . . 18
โข
(โfld โ Ring โ โfld โ
CMnd) |
102 | 100, 101 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
โข
โfld โ CMnd |
103 | 90 | submcmn 19623 |
. . . . . . . . . . . . . . . . 17
โข
((โfld โ CMnd โง โ0 โ
(SubMndโโfld)) โ (โfld
โพs โ0) โ CMnd) |
104 | 102, 89, 103 | mp2an 691 |
. . . . . . . . . . . . . . . 16
โข
(โfld โพs โ0) โ
CMnd |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (โfld
โพs โ0) โ CMnd) |
106 | 7 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ผ โ ๐) |
107 | 5 | psrbagf 21336 |
. . . . . . . . . . . . . . . 16
โข (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ ๐:๐ผโถโ0) |
108 | 83, 107 | syl 17 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐:๐ผโถโ0) |
109 | | simpllr 775 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ
Fin}) |
110 | 5 | psrbagf 21336 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ ๐ฅ:๐ผโถโ0) |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ฅ:๐ผโถโ0) |
112 | 111 | ffnd 6674 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ฅ Fn ๐ผ) |
113 | 108 | ffnd 6674 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ Fn ๐ผ) |
114 | | inidm 4183 |
. . . . . . . . . . . . . . . . 17
โข (๐ผ โฉ ๐ผ) = ๐ผ |
115 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐ฅโ๐) = (๐ฅโ๐)) |
116 | | eqidd 2738 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐โ๐) = (๐โ๐)) |
117 | 112, 113,
106, 106, 114, 115, 116 | offval 7631 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ฅ โf โ ๐) = (๐ โ ๐ผ โฆ ((๐ฅโ๐) โ (๐โ๐)))) |
118 | | simpl 484 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ})) |
119 | | simplr 768 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) |
120 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ (๐ โr โค ๐ฅ โ ๐ โr โค ๐ฅ)) |
121 | 120 | elrab 3650 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โ (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โง ๐ โr โค ๐ฅ)) |
122 | 121 | simprbi 498 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โ ๐ โr โค ๐ฅ) |
123 | 119, 122 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ๐ โr โค ๐ฅ) |
124 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ๐ โ ๐ผ) |
125 | 113, 112,
106, 106, 114, 116, 115 | ofrval 7634 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โr โค ๐ฅ โง ๐ โ ๐ผ) โ (๐โ๐) โค (๐ฅโ๐)) |
126 | 118, 123,
124, 125 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐โ๐) โค (๐ฅโ๐)) |
127 | 108 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐โ๐) โ
โ0) |
128 | 111 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐ฅโ๐) โ
โ0) |
129 | | nn0sub 12470 |
. . . . . . . . . . . . . . . . . 18
โข (((๐โ๐) โ โ0 โง (๐ฅโ๐) โ โ0) โ ((๐โ๐) โค (๐ฅโ๐) โ ((๐ฅโ๐) โ (๐โ๐)) โ
โ0)) |
130 | 127, 128,
129 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ((๐โ๐) โค (๐ฅโ๐) โ ((๐ฅโ๐) โ (๐โ๐)) โ
โ0)) |
131 | 126, 130 | mpbid 231 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ((๐ฅโ๐) โ (๐โ๐)) โ
โ0) |
132 | 117, 131 | fmpt3d 7069 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ฅ โf โ ๐):๐ผโถโ0) |
133 | 108 | ffund 6677 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ Fun ๐) |
134 | | c0ex 11156 |
. . . . . . . . . . . . . . . . . . . 20
โข 0 โ
V |
135 | 106, 134 | jctir 522 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ผ โ ๐ โง 0 โ V)) |
136 | | fsuppeq 8111 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ผ โ ๐ โง 0 โ V) โ (๐:๐ผโถโ0 โ (๐ supp 0) = (โก๐ โ (โ0 โ
{0})))) |
137 | 135, 108,
136 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ supp 0) = (โก๐ โ (โ0 โ
{0}))) |
138 | | dfn2 12433 |
. . . . . . . . . . . . . . . . . . 19
โข โ =
(โ0 โ {0}) |
139 | 138 | imaeq2i 6016 |
. . . . . . . . . . . . . . . . . 18
โข (โก๐ โ โ) = (โก๐ โ (โ0 โ
{0})) |
140 | 137, 139 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ supp 0) = (โก๐ โ โ)) |
141 | 5 | psrbag 21335 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ผ โ ๐ โ (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ (๐:๐ผโถโ0 โง (โก๐ โ โ) โ
Fin))) |
142 | 106, 141 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ (๐:๐ผโถโ0 โง (โก๐ โ โ) โ
Fin))) |
143 | 83, 142 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐:๐ผโถโ0 โง (โก๐ โ โ) โ
Fin)) |
144 | 143 | simprd 497 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (โก๐ โ โ) โ
Fin) |
145 | 140, 144 | eqeltrd 2838 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ supp 0) โ Fin) |
146 | 83 | elexd 3468 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ โ V) |
147 | | isfsupp 9316 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โ V โง 0 โ V)
โ (๐ finSupp 0 โ
(Fun ๐ โง (๐ supp 0) โ
Fin))) |
148 | 146, 134,
147 | sylancl 587 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ finSupp 0 โ (Fun ๐ โง (๐ supp 0) โ Fin))) |
149 | 133, 145,
148 | mpbir2and 712 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ finSupp 0) |
150 | 112, 113,
106, 106 | offun 7636 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ Fun (๐ฅ โf โ
๐)) |
151 | 5 | psrbagfsupp 21338 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โ ๐ฅ finSupp 0) |
152 | 109, 151 | syl 17 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ฅ finSupp 0) |
153 | 152, 149 | fsuppunfi 9332 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ((๐ฅ supp 0) โช (๐ supp 0)) โ Fin) |
154 | | 0nn0 12435 |
. . . . . . . . . . . . . . . . . . 19
โข 0 โ
โ0 |
155 | 154 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ 0 โ
โ0) |
156 | | 0m0e0 12280 |
. . . . . . . . . . . . . . . . . . 19
โข (0
โ 0) = 0 |
157 | 156 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (0 โ 0) =
0) |
158 | 106, 155,
111, 108, 157 | suppofssd 8139 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ((๐ฅ โf โ ๐) supp 0) โ ((๐ฅ supp 0) โช (๐ supp 0))) |
159 | 153, 158 | ssfid 9218 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ((๐ฅ โf โ ๐) supp 0) โ
Fin) |
160 | | ovexd 7397 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ฅ โf โ ๐) โ V) |
161 | | isfsupp 9316 |
. . . . . . . . . . . . . . . . 17
โข (((๐ฅ โf โ
๐) โ V โง 0 โ
V) โ ((๐ฅ
โf โ ๐) finSupp 0 โ (Fun (๐ฅ โf โ ๐) โง ((๐ฅ โf โ ๐) supp 0) โ
Fin))) |
162 | 160, 134,
161 | sylancl 587 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ((๐ฅ โf โ ๐) finSupp 0 โ (Fun (๐ฅ โf โ
๐) โง ((๐ฅ โf โ
๐) supp 0) โ
Fin))) |
163 | 150, 159,
162 | mpbir2and 712 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ฅ โf โ ๐) finSupp 0) |
164 | 92, 95, 99, 105, 106, 108, 132, 149, 163 | gsumadd 19707 |
. . . . . . . . . . . . . 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 โ
๐)))) |
165 | 108 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐โ๐) โ
โ0) |
166 | 165 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐โ๐) โ โ) |
167 | 111 | ffvelcdmda 7040 |
. . . . . . . . . . . . . . . . . . 19
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐ฅโ๐) โ
โ0) |
168 | 167 | nn0cnd 12482 |
. . . . . . . . . . . . . . . . . 18
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐ฅโ๐) โ โ) |
169 | 166, 168 | pncan3d 11522 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ((๐โ๐) + ((๐ฅโ๐) โ (๐โ๐))) = (๐ฅโ๐)) |
170 | 169 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ โ ๐ผ โฆ ((๐โ๐) + ((๐ฅโ๐) โ (๐โ๐)))) = (๐ โ ๐ผ โฆ (๐ฅโ๐))) |
171 | | fvexd 6862 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ (๐โ๐) โ V) |
172 | | ovexd 7397 |
. . . . . . . . . . . . . . . . 17
โข
(((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โง ๐ โ ๐ผ) โ ((๐ฅโ๐) โ (๐โ๐)) โ V) |
173 | 108 | feqmptd 6915 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ = (๐ โ ๐ผ โฆ (๐โ๐))) |
174 | 111 | feqmptd 6915 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ๐ฅ = (๐ โ ๐ผ โฆ (๐ฅโ๐))) |
175 | 106, 167,
165, 174, 173 | offval2 7642 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ฅ โf โ ๐) = (๐ โ ๐ผ โฆ ((๐ฅโ๐) โ (๐โ๐)))) |
176 | 106, 171,
172, 173, 175 | offval2 7642 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ โf + (๐ฅ โf โ ๐)) = (๐ โ ๐ผ โฆ ((๐โ๐) + ((๐ฅโ๐) โ (๐โ๐))))) |
177 | 170, 176,
174 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . 15
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ (๐ โf + (๐ฅ โf โ ๐)) = ๐ฅ) |
178 | 177 | oveq2d 7378 |
. . . . . . . . . . . . . 14
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ
((โfld โพs โ0)
ฮฃg (๐ โf + (๐ฅ โf โ ๐))) = ((โfld
โพs โ0) ฮฃg ๐ฅ)) |
179 | 164, 178 | eqtr3d 2779 |
. . . . . . . . . . . . 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 ๐ฅ)) |
180 | | simplr 768 |
. . . . . . . . . . . . 13
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) |
181 | 179, 180 | eqnetrd 3012 |
. . . . . . . . . . . 12
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ
(((โfld โพs โ0)
ฮฃg ๐) + ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐))) โ (๐ + ๐)) |
182 | | oveq12 7371 |
. . . . . . . . . . . . . 14
โข
((((โfld โพs โ0)
ฮฃg ๐) = ๐ โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) = ๐) โ (((โfld
โพs โ0) ฮฃg ๐) + ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐))) = (๐ + ๐)) |
183 | 182 | 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 โ
๐))) = (๐ + ๐))) |
184 | 183 | necon3ad 2957 |
. . . . . . . . . . . 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 โ
๐)) = ๐))) |
185 | 181, 184 | mpd 15 |
. . . . . . . . . . 11
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ยฌ
(((โfld โพs โ0)
ฮฃg ๐) = ๐ โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) = ๐)) |
186 | | neorian 3040 |
. . . . . . . . . . 11
โข
((((โfld โพs โ0)
ฮฃg ๐) โ ๐ โจ ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐) โ ยฌ (((โfld
โพs โ0) ฮฃg ๐) = ๐ โง ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) = ๐)) |
187 | 185, 186 | sylibr 233 |
. . . . . . . . . 10
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ
(((โfld โพs โ0)
ฮฃg ๐) โ ๐ โจ ((โfld
โพs โ0) ฮฃg (๐ฅ โf โ
๐)) โ ๐)) |
188 | 62, 88, 187 | mpjaodan 958 |
. . . . . . . . 9
โข ((((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โง ๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ}) โ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))) = (0gโ๐
)) |
189 | 188 | mpteq2dva 5210 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โ (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐)))) = (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ
(0gโ๐
))) |
190 | 189 | oveq2d 7378 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) = (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ
(0gโ๐
)))) |
191 | | ringmnd 19981 |
. . . . . . . . . 10
โข (๐
โ Ring โ ๐
โ Mnd) |
192 | 8, 191 | syl 17 |
. . . . . . . . 9
โข (๐ โ ๐
โ Mnd) |
193 | 192 | ad2antrr 725 |
. . . . . . . 8
โข (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โ ๐
โ Mnd) |
194 | 44 | rabex 5294 |
. . . . . . . 8
โข {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โ V |
195 | 41 | gsumz 18653 |
. . . . . . . 8
โข ((๐
โ Mnd โง {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โ V) โ (๐
ฮฃg
(๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ
(0gโ๐
))) =
(0gโ๐
)) |
196 | 193, 194,
195 | sylancl 587 |
. . . . . . 7
โข (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ
(0gโ๐
))) =
(0gโ๐
)) |
197 | 190, 196 | eqtrd 2777 |
. . . . . 6
โข (((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โง
((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐)) โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) =
(0gโ๐
)) |
198 | 197 | ex 414 |
. . . . 5
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ
(((โfld โพs โ0)
ฮฃg ๐ฅ) โ (๐ + ๐) โ (๐
ฮฃg (๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) =
(0gโ๐
))) |
199 | 198 | necon1d 2966 |
. . . 4
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ ((๐
ฮฃg
(๐ โ {๐ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} โฃ ๐ โr โค ๐ฅ} โฆ ((๐โ๐)(.rโ๐
)(๐โ(๐ฅ โf โ ๐))))) โ
(0gโ๐
)
โ ((โfld โพs โ0)
ฮฃg ๐ฅ) = (๐ + ๐))) |
200 | 27, 199 | sylbid 239 |
. . 3
โข ((๐ โง ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin}) โ (((๐ ยท ๐)โ๐ฅ) โ (0gโ๐
) โ ((โfld
โพs โ0) ฮฃg ๐ฅ) = (๐ + ๐))) |
201 | 200 | ralrimiva 3144 |
. 2
โข (๐ โ โ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} (((๐ ยท ๐)โ๐ฅ) โ (0gโ๐
) โ ((โfld
โพs โ0) ฮฃg ๐ฅ) = (๐ + ๐))) |
202 | 9, 12 | nn0addcld 12484 |
. . 3
โข (๐ โ (๐ + ๐) โ
โ0) |
203 | 1 | mplring 21440 |
. . . . 5
โข ((๐ผ โ ๐ โง ๐
โ Ring) โ ๐ โ Ring) |
204 | 7, 8, 203 | syl2anc 585 |
. . . 4
โข (๐ โ ๐ โ Ring) |
205 | 2, 4 | ringcl 19988 |
. . . 4
โข ((๐ โ Ring โง ๐ โ (Baseโ๐) โง ๐ โ (Baseโ๐)) โ (๐ ยท ๐) โ (Baseโ๐)) |
206 | 204, 11, 14, 205 | syl3anc 1372 |
. . 3
โข (๐ โ (๐ ยท ๐) โ (Baseโ๐)) |
207 | 6, 1, 2, 41, 5, 7,
8, 202, 206 | ismhp3 21549 |
. 2
โข (๐ โ ((๐ ยท ๐) โ (๐ปโ(๐ + ๐)) โ โ๐ฅ โ {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} (((๐ ยท ๐)โ๐ฅ) โ (0gโ๐
) โ ((โfld
โพs โ0) ฮฃg ๐ฅ) = (๐ + ๐)))) |
208 | 201, 207 | mpbird 257 |
1
โข (๐ โ (๐ ยท ๐) โ (๐ปโ(๐ + ๐))) |