Step | Hyp | Ref
| Expression |
1 | | evlslem1.s |
. . . . . 6
โข (๐ โ ๐ โ CRing) |
2 | | crngring 20067 |
. . . . . 6
โข (๐ โ CRing โ ๐ โ Ring) |
3 | 1, 2 | syl 17 |
. . . . 5
โข (๐ โ ๐ โ Ring) |
4 | 3 | adantr 481 |
. . . 4
โข ((๐ โง ๐ โ ๐ท) โ ๐ โ Ring) |
5 | | evlslem1.f |
. . . . . . 7
โข (๐ โ ๐น โ (๐
RingHom ๐)) |
6 | | eqid 2732 |
. . . . . . . 8
โข
(Baseโ๐
) =
(Baseโ๐
) |
7 | | evlslem1.c |
. . . . . . . 8
โข ๐ถ = (Baseโ๐) |
8 | 6, 7 | rhmf 20262 |
. . . . . . 7
โข (๐น โ (๐
RingHom ๐) โ ๐น:(Baseโ๐
)โถ๐ถ) |
9 | 5, 8 | syl 17 |
. . . . . 6
โข (๐ โ ๐น:(Baseโ๐
)โถ๐ถ) |
10 | 9 | adantr 481 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ ๐น:(Baseโ๐
)โถ๐ถ) |
11 | | evlslem1.p |
. . . . . . 7
โข ๐ = (๐ผ mPoly ๐
) |
12 | | evlslem1.b |
. . . . . . 7
โข ๐ต = (Baseโ๐) |
13 | | evlslem1.d |
. . . . . . 7
โข ๐ท = {โ โ (โ0
โm ๐ผ)
โฃ (โกโ โ โ) โ Fin} |
14 | | evlslem6.y |
. . . . . . 7
โข (๐ โ ๐ โ ๐ต) |
15 | 11, 6, 12, 13, 14 | mplelf 21556 |
. . . . . 6
โข (๐ โ ๐:๐ทโถ(Baseโ๐
)) |
16 | 15 | ffvelcdmda 7086 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ (๐โ๐) โ (Baseโ๐
)) |
17 | 10, 16 | ffvelcdmd 7087 |
. . . 4
โข ((๐ โง ๐ โ ๐ท) โ (๐นโ(๐โ๐)) โ ๐ถ) |
18 | | evlslem1.t |
. . . . . 6
โข ๐ = (mulGrpโ๐) |
19 | 18, 7 | mgpbas 19992 |
. . . . 5
โข ๐ถ = (Baseโ๐) |
20 | | evlslem1.x |
. . . . 5
โข โ =
(.gโ๐) |
21 | 18 | crngmgp 20063 |
. . . . . . 7
โข (๐ โ CRing โ ๐ โ CMnd) |
22 | 1, 21 | syl 17 |
. . . . . 6
โข (๐ โ ๐ โ CMnd) |
23 | 22 | adantr 481 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ ๐ โ CMnd) |
24 | | simpr 485 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ ๐ โ ๐ท) |
25 | | evlslem1.g |
. . . . . 6
โข (๐ โ ๐บ:๐ผโถ๐ถ) |
26 | 25 | adantr 481 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ ๐บ:๐ผโถ๐ถ) |
27 | 13, 19, 20, 23, 24, 26 | psrbagev2 21639 |
. . . 4
โข ((๐ โง ๐ โ ๐ท) โ (๐ ฮฃg (๐ โf โ ๐บ)) โ ๐ถ) |
28 | | evlslem1.m |
. . . . 5
โข ยท =
(.rโ๐) |
29 | 7, 28 | ringcl 20072 |
. . . 4
โข ((๐ โ Ring โง (๐นโ(๐โ๐)) โ ๐ถ โง (๐ ฮฃg (๐ โf โ ๐บ)) โ ๐ถ) โ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ))) โ ๐ถ) |
30 | 4, 17, 27, 29 | syl3anc 1371 |
. . 3
โข ((๐ โง ๐ โ ๐ท) โ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ))) โ ๐ถ) |
31 | 30 | fmpttd 7114 |
. 2
โข (๐ โ (๐ โ ๐ท โฆ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ)))):๐ทโถ๐ถ) |
32 | | ovexd 7443 |
. . . . 5
โข (๐ โ (โ0
โm ๐ผ)
โ V) |
33 | 13, 32 | rabexd 5333 |
. . . 4
โข (๐ โ ๐ท โ V) |
34 | 33 | mptexd 7225 |
. . 3
โข (๐ โ (๐ โ ๐ท โฆ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ)))) โ V) |
35 | | funmpt 6586 |
. . . 4
โข Fun
(๐ โ ๐ท โฆ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ)))) |
36 | 35 | a1i 11 |
. . 3
โข (๐ โ Fun (๐ โ ๐ท โฆ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ))))) |
37 | | fvexd 6906 |
. . 3
โข (๐ โ (0gโ๐) โ V) |
38 | | eqid 2732 |
. . . . 5
โข
(0gโ๐
) = (0gโ๐
) |
39 | | evlslem1.r |
. . . . 5
โข (๐ โ ๐
โ CRing) |
40 | 11, 12, 38, 14, 39 | mplelsfi 21553 |
. . . 4
โข (๐ โ ๐ finSupp (0gโ๐
)) |
41 | 40 | fsuppimpd 9368 |
. . 3
โข (๐ โ (๐ supp (0gโ๐
)) โ Fin) |
42 | 15 | feqmptd 6960 |
. . . . . . 7
โข (๐ โ ๐ = (๐ โ ๐ท โฆ (๐โ๐))) |
43 | 42 | oveq1d 7423 |
. . . . . 6
โข (๐ โ (๐ supp (0gโ๐
)) = ((๐ โ ๐ท โฆ (๐โ๐)) supp (0gโ๐
))) |
44 | | eqimss2 4041 |
. . . . . 6
โข ((๐ supp (0gโ๐
)) = ((๐ โ ๐ท โฆ (๐โ๐)) supp (0gโ๐
)) โ ((๐ โ ๐ท โฆ (๐โ๐)) supp (0gโ๐
)) โ (๐ supp (0gโ๐
))) |
45 | 43, 44 | syl 17 |
. . . . 5
โข (๐ โ ((๐ โ ๐ท โฆ (๐โ๐)) supp (0gโ๐
)) โ (๐ supp (0gโ๐
))) |
46 | | rhmghm 20261 |
. . . . . 6
โข (๐น โ (๐
RingHom ๐) โ ๐น โ (๐
GrpHom ๐)) |
47 | | eqid 2732 |
. . . . . . 7
โข
(0gโ๐) = (0gโ๐) |
48 | 38, 47 | ghmid 19097 |
. . . . . 6
โข (๐น โ (๐
GrpHom ๐) โ (๐นโ(0gโ๐
)) = (0gโ๐)) |
49 | 5, 46, 48 | 3syl 18 |
. . . . 5
โข (๐ โ (๐นโ(0gโ๐
)) = (0gโ๐)) |
50 | | fvexd 6906 |
. . . . 5
โข ((๐ โง ๐ โ ๐ท) โ (๐โ๐) โ V) |
51 | | fvexd 6906 |
. . . . 5
โข (๐ โ (0gโ๐
) โ V) |
52 | 45, 49, 50, 51 | suppssfv 8186 |
. . . 4
โข (๐ โ ((๐ โ ๐ท โฆ (๐นโ(๐โ๐))) supp (0gโ๐)) โ (๐ supp (0gโ๐
))) |
53 | 7, 28, 47 | ringlz 20106 |
. . . . 5
โข ((๐ โ Ring โง ๐ฅ โ ๐ถ) โ ((0gโ๐) ยท ๐ฅ) = (0gโ๐)) |
54 | 3, 53 | sylan 580 |
. . . 4
โข ((๐ โง ๐ฅ โ ๐ถ) โ ((0gโ๐) ยท ๐ฅ) = (0gโ๐)) |
55 | | fvexd 6906 |
. . . 4
โข ((๐ โง ๐ โ ๐ท) โ (๐นโ(๐โ๐)) โ V) |
56 | 52, 54, 55, 27, 37 | suppssov1 8182 |
. . 3
โข (๐ โ ((๐ โ ๐ท โฆ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ)))) supp
(0gโ๐))
โ (๐ supp
(0gโ๐
))) |
57 | | suppssfifsupp 9377 |
. . 3
โข ((((๐ โ ๐ท โฆ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ)))) โ V โง Fun (๐ โ ๐ท โฆ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ)))) โง
(0gโ๐)
โ V) โง ((๐ supp
(0gโ๐
))
โ Fin โง ((๐ โ
๐ท โฆ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ)))) supp
(0gโ๐))
โ (๐ supp
(0gโ๐
))))
โ (๐ โ ๐ท โฆ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ)))) finSupp
(0gโ๐)) |
58 | 34, 36, 37, 41, 56, 57 | syl32anc 1378 |
. 2
โข (๐ โ (๐ โ ๐ท โฆ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ)))) finSupp
(0gโ๐)) |
59 | 31, 58 | jca 512 |
1
โข (๐ โ ((๐ โ ๐ท โฆ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ)))):๐ทโถ๐ถ โง (๐ โ ๐ท โฆ ((๐นโ(๐โ๐)) ยท (๐ ฮฃg (๐ โf โ ๐บ)))) finSupp
(0gโ๐))) |