Step | Hyp | Ref
| Expression |
1 | | elply 25572 |
. . . . 5
β’ (π β (Polyβπ) β (π β β β§ βπ β β0
βπ β ((π βͺ {0}) βm
β0)π =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ))))) |
2 | 1 | simprbi 498 |
. . . 4
β’ (π β (Polyβπ) β βπ β β0
βπ β ((π βͺ {0}) βm
β0)π =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) |
3 | | eqid 2737 |
. . . . . . . . 9
β’
(βfld βs β) =
(βfld βs β) |
4 | | cnfldbas 20816 |
. . . . . . . . 9
β’ β =
(Baseββfld) |
5 | | eqid 2737 |
. . . . . . . . 9
β’
(0gβ(βfld βs
β)) = (0gβ(βfld
βs β)) |
6 | | cnex 11139 |
. . . . . . . . . 10
β’ β
β V |
7 | 6 | a1i 11 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β β β V) |
8 | | fzfid 13885 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (0...π) β Fin) |
9 | | cnring 20835 |
. . . . . . . . . 10
β’
βfld β Ring |
10 | | ringcmn 20010 |
. . . . . . . . . 10
β’
(βfld β Ring β βfld β
CMnd) |
11 | 9, 10 | mp1i 13 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β βfld β
CMnd) |
12 | 4 | subrgss 20239 |
. . . . . . . . . . . . 13
β’ (π β
(SubRingββfld) β π β β) |
13 | 12 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β π β β) |
14 | | elmapi 8794 |
. . . . . . . . . . . . . . 15
β’ (π β ((π βͺ {0}) βm
β0) β π:β0βΆ(π βͺ {0})) |
15 | 14 | ad2antll 728 |
. . . . . . . . . . . . . 14
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β π:β0βΆ(π βͺ {0})) |
16 | | subrgsubg 20244 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(SubRingββfld) β π β
(SubGrpββfld)) |
17 | | cnfld0 20837 |
. . . . . . . . . . . . . . . . . . . 20
β’ 0 =
(0gββfld) |
18 | 17 | subg0cl 18943 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(SubGrpββfld) β 0 β π) |
19 | 16, 18 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β
(SubRingββfld) β 0 β π) |
20 | 19 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β 0 β π) |
21 | 20 | snssd 4774 |
. . . . . . . . . . . . . . . 16
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β {0} β π) |
22 | | ssequn2 4148 |
. . . . . . . . . . . . . . . 16
β’ ({0}
β π β (π βͺ {0}) = π) |
23 | 21, 22 | sylib 217 |
. . . . . . . . . . . . . . 15
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (π βͺ {0}) = π) |
24 | 23 | feq3d 6660 |
. . . . . . . . . . . . . 14
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (π:β0βΆ(π βͺ {0}) β π:β0βΆπ)) |
25 | 15, 24 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β π:β0βΆπ) |
26 | | elfznn0 13541 |
. . . . . . . . . . . . 13
β’ (π β (0...π) β π β β0) |
27 | | ffvelcdm 7037 |
. . . . . . . . . . . . 13
β’ ((π:β0βΆπ β§ π β β0) β (πβπ) β π) |
28 | 25, 26, 27 | syl2an 597 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (πβπ) β π) |
29 | 13, 28 | sseldd 3950 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (πβπ) β β) |
30 | 29 | adantrl 715 |
. . . . . . . . . 10
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ (π§ β β β§ π β (0...π))) β (πβπ) β β) |
31 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ (π§ β β β§ π β (0...π))) β π§ β β) |
32 | 26 | ad2antll 728 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ (π§ β β β§ π β (0...π))) β π β β0) |
33 | | expcl 13992 |
. . . . . . . . . . 11
β’ ((π§ β β β§ π β β0)
β (π§βπ) β
β) |
34 | 31, 32, 33 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ (π§ β β β§ π β (0...π))) β (π§βπ) β β) |
35 | 30, 34 | mulcld 11182 |
. . . . . . . . 9
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ (π§ β β β§ π β (0...π))) β ((πβπ) Β· (π§βπ)) β β) |
36 | | eqid 2737 |
. . . . . . . . . 10
β’ (π β (0...π) β¦ (π§ β β β¦ ((πβπ) Β· (π§βπ)))) = (π β (0...π) β¦ (π§ β β β¦ ((πβπ) Β· (π§βπ)))) |
37 | 6 | mptex 7178 |
. . . . . . . . . . 11
β’ (π§ β β β¦ ((πβπ) Β· (π§βπ))) β V |
38 | 37 | a1i 11 |
. . . . . . . . . 10
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (π§ β β β¦ ((πβπ) Β· (π§βπ))) β V) |
39 | | fvex 6860 |
. . . . . . . . . . 11
β’
(0gβ(βfld βs
β)) β V |
40 | 39 | a1i 11 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (0gβ(βfld
βs β)) β V) |
41 | 36, 8, 38, 40 | fsuppmptdm 9323 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (π β (0...π) β¦ (π§ β β β¦ ((πβπ) Β· (π§βπ)))) finSupp
(0gβ(βfld βs
β))) |
42 | 3, 4, 5, 7, 8, 11,
35, 41 | pwsgsum 19766 |
. . . . . . . 8
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β ((βfld βs
β) Ξ£g (π β (0...π) β¦ (π§ β β β¦ ((πβπ) Β· (π§βπ))))) = (π§ β β β¦
(βfld Ξ£g (π β (0...π) β¦ ((πβπ) Β· (π§βπ)))))) |
43 | | fzfid 13885 |
. . . . . . . . . 10
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β (0...π) β Fin) |
44 | 35 | anassrs 469 |
. . . . . . . . . 10
β’ ((((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β§ π β (0...π)) β ((πβπ) Β· (π§βπ)) β β) |
45 | 43, 44 | gsumfsum 20880 |
. . . . . . . . 9
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π§ β β) β
(βfld Ξ£g (π β (0...π) β¦ ((πβπ) Β· (π§βπ)))) = Ξ£π β (0...π)((πβπ) Β· (π§βπ))) |
46 | 45 | mpteq2dva 5210 |
. . . . . . . 8
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (π§ β β β¦
(βfld Ξ£g (π β (0...π) β¦ ((πβπ) Β· (π§βπ))))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) |
47 | 42, 46 | eqtrd 2777 |
. . . . . . 7
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β ((βfld βs
β) Ξ£g (π β (0...π) β¦ (π§ β β β¦ ((πβπ) Β· (π§βπ))))) = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ)))) |
48 | 3 | pwsring 20046 |
. . . . . . . . . 10
β’
((βfld β Ring β§ β β V) β
(βfld βs β) β
Ring) |
49 | 9, 6, 48 | mp2an 691 |
. . . . . . . . 9
β’
(βfld βs β) β
Ring |
50 | | ringcmn 20010 |
. . . . . . . . 9
β’
((βfld βs β) β Ring
β (βfld βs β) β
CMnd) |
51 | 49, 50 | mp1i 13 |
. . . . . . . 8
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (βfld βs
β) β CMnd) |
52 | | cncrng 20834 |
. . . . . . . . . . 11
β’
βfld β CRing |
53 | | plypf1.e |
. . . . . . . . . . . 12
β’ πΈ =
(eval1ββfld) |
54 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(Poly1ββfld) =
(Poly1ββfld) |
55 | 53, 54, 3, 4 | evl1rhm 21714 |
. . . . . . . . . . 11
β’
(βfld β CRing β πΈ β
((Poly1ββfld) RingHom (βfld
βs β))) |
56 | 52, 55 | ax-mp 5 |
. . . . . . . . . 10
β’ πΈ β
((Poly1ββfld) RingHom (βfld
βs β)) |
57 | | plypf1.r |
. . . . . . . . . . . 12
β’ π
= (βfld
βΎs π) |
58 | | plypf1.p |
. . . . . . . . . . . 12
β’ π = (Poly1βπ
) |
59 | | plypf1.a |
. . . . . . . . . . . 12
β’ π΄ = (Baseβπ) |
60 | 54, 57, 58, 59 | subrgply1 21620 |
. . . . . . . . . . 11
β’ (π β
(SubRingββfld) β π΄ β
(SubRingβ(Poly1ββfld))) |
61 | 60 | adantr 482 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β π΄ β
(SubRingβ(Poly1ββfld))) |
62 | | rhmima 20269 |
. . . . . . . . . 10
β’ ((πΈ β
((Poly1ββfld) RingHom (βfld
βs β)) β§ π΄ β
(SubRingβ(Poly1ββfld))) β (πΈ β π΄) β
(SubRingβ(βfld βs
β))) |
63 | 56, 61, 62 | sylancr 588 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (πΈ β π΄) β
(SubRingβ(βfld βs
β))) |
64 | | subrgsubg 20244 |
. . . . . . . . 9
β’ ((πΈ β π΄) β
(SubRingβ(βfld βs β))
β (πΈ β π΄) β
(SubGrpβ(βfld βs
β))) |
65 | | subgsubm 18957 |
. . . . . . . . 9
β’ ((πΈ β π΄) β
(SubGrpβ(βfld βs β)) β
(πΈ β π΄) β
(SubMndβ(βfld βs
β))) |
66 | 63, 64, 65 | 3syl 18 |
. . . . . . . 8
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (πΈ β π΄) β
(SubMndβ(βfld βs
β))) |
67 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(Baseβ(βfld βs β)) =
(Baseβ(βfld βs
β)) |
68 | 9 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β βfld β
Ring) |
69 | 6 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β β β V) |
70 | | fconst6g 6736 |
. . . . . . . . . . . . . 14
β’ ((πβπ) β β β (β Γ
{(πβπ)}):ββΆβ) |
71 | 29, 70 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (β Γ {(πβπ)}):ββΆβ) |
72 | 3, 4, 67 | pwselbasb 17377 |
. . . . . . . . . . . . . 14
β’
((βfld β Ring β§ β β V) β
((β Γ {(πβπ)}) β (Baseβ(βfld
βs β)) β (β Γ {(πβπ)}):ββΆβ)) |
73 | 9, 6, 72 | mp2an 691 |
. . . . . . . . . . . . 13
β’ ((β
Γ {(πβπ)}) β
(Baseβ(βfld βs β)) β
(β Γ {(πβπ)}):ββΆβ) |
74 | 71, 73 | sylibr 233 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (β Γ {(πβπ)}) β (Baseβ(βfld
βs β))) |
75 | 34 | anass1rs 654 |
. . . . . . . . . . . . . 14
β’ ((((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β§ π§ β β) β (π§βπ) β β) |
76 | 75 | fmpttd 7068 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (π§ β β β¦ (π§βπ)):ββΆβ) |
77 | 3, 4, 67 | pwselbasb 17377 |
. . . . . . . . . . . . . 14
β’
((βfld β Ring β§ β β V) β
((π§ β β β¦
(π§βπ)) β (Baseβ(βfld
βs β)) β (π§ β β β¦ (π§βπ)):ββΆβ)) |
78 | 9, 6, 77 | mp2an 691 |
. . . . . . . . . . . . 13
β’ ((π§ β β β¦ (π§βπ)) β (Baseβ(βfld
βs β)) β (π§ β β β¦ (π§βπ)):ββΆβ) |
79 | 76, 78 | sylibr 233 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (π§ β β β¦ (π§βπ)) β (Baseβ(βfld
βs β))) |
80 | | cnfldmul 20818 |
. . . . . . . . . . . 12
β’ Β·
= (.rββfld) |
81 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(.rβ(βfld βs
β)) = (.rβ(βfld
βs β)) |
82 | 3, 67, 68, 69, 74, 79, 80, 81 | pwsmulrval 17380 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β ((β Γ {(πβπ)})(.rβ(βfld
βs β))(π§ β β β¦ (π§βπ))) = ((β Γ {(πβπ)}) βf Β· (π§ β β β¦ (π§βπ)))) |
83 | 29 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β§ π§ β β) β (πβπ) β β) |
84 | | fconstmpt 5699 |
. . . . . . . . . . . . 13
β’ (β
Γ {(πβπ)}) = (π§ β β β¦ (πβπ)) |
85 | 84 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (β Γ {(πβπ)}) = (π§ β β β¦ (πβπ))) |
86 | | eqidd 2738 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (π§ β β β¦ (π§βπ)) = (π§ β β β¦ (π§βπ))) |
87 | 69, 83, 75, 85, 86 | offval2 7642 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β ((β Γ {(πβπ)}) βf Β· (π§ β β β¦ (π§βπ))) = (π§ β β β¦ ((πβπ) Β· (π§βπ)))) |
88 | 82, 87 | eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β ((β Γ {(πβπ)})(.rβ(βfld
βs β))(π§ β β β¦ (π§βπ))) = (π§ β β β¦ ((πβπ) Β· (π§βπ)))) |
89 | 63 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (πΈ β π΄) β
(SubRingβ(βfld βs
β))) |
90 | | eqid 2737 |
. . . . . . . . . . . . . 14
β’
(algScβ(Poly1ββfld)) =
(algScβ(Poly1ββfld)) |
91 | 53, 54, 4, 90 | evl1sca 21716 |
. . . . . . . . . . . . 13
β’
((βfld β CRing β§ (πβπ) β β) β (πΈβ((algScβ(Poly1ββfld))β(πβπ))) =
(β Γ {(πβπ)})) |
92 | 52, 29, 91 | sylancr 588 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (πΈβ((algScβ(Poly1ββfld))β(πβπ))) =
(β Γ {(πβπ)})) |
93 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
β’
(Baseβ(Poly1ββfld)) =
(Baseβ(Poly1ββfld)) |
94 | 93, 67 | rhmf 20167 |
. . . . . . . . . . . . . . 15
β’ (πΈ β
((Poly1ββfld) RingHom (βfld
βs β)) β πΈ:(Baseβ(Poly1ββfld))βΆ(Baseβ(βfld
βs β))) |
95 | 56, 94 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ πΈ:(Baseβ(Poly1ββfld))βΆ(Baseβ(βfld
βs β)) |
96 | | ffn 6673 |
. . . . . . . . . . . . . 14
β’ (πΈ:(Baseβ(Poly1ββfld))βΆ(Baseβ(βfld
βs β)) β πΈ Fn
(Baseβ(Poly1ββfld))) |
97 | 95, 96 | mp1i 13 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β πΈ Fn
(Baseβ(Poly1ββfld))) |
98 | 93 | subrgss 20239 |
. . . . . . . . . . . . . . 15
β’ (π΄ β
(SubRingβ(Poly1ββfld)) β π΄ β
(Baseβ(Poly1ββfld))) |
99 | 60, 98 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β
(SubRingββfld) β π΄ β
(Baseβ(Poly1ββfld))) |
100 | 99 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β π΄ β
(Baseβ(Poly1ββfld))) |
101 | | simpll 766 |
. . . . . . . . . . . . . . 15
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β π β
(SubRingββfld)) |
102 | 54, 90, 57, 58, 101, 59, 4, 29 | subrg1asclcl 21647 |
. . . . . . . . . . . . . 14
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β
(((algScβ(Poly1ββfld))β(πβπ)) β π΄ β (πβπ) β π)) |
103 | 28, 102 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β
((algScβ(Poly1ββfld))β(πβπ)) β π΄) |
104 | | fnfvima 7188 |
. . . . . . . . . . . . 13
β’ ((πΈ Fn
(Baseβ(Poly1ββfld)) β§ π΄ β
(Baseβ(Poly1ββfld)) β§
((algScβ(Poly1ββfld))β(πβπ)) β π΄) β (πΈβ((algScβ(Poly1ββfld))β(πβπ)))
β (πΈ β π΄)) |
105 | 97, 100, 103, 104 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (πΈβ((algScβ(Poly1ββfld))β(πβπ)))
β (πΈ β π΄)) |
106 | 92, 105 | eqeltrrd 2839 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (β Γ {(πβπ)}) β (πΈ β π΄)) |
107 | 67 | subrgss 20239 |
. . . . . . . . . . . . . . . . 17
β’ ((πΈ β π΄) β
(SubRingβ(βfld βs β))
β (πΈ β π΄) β
(Baseβ(βfld βs
β))) |
108 | 89, 107 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (πΈ β π΄) β (Baseβ(βfld
βs β))) |
109 | 60 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β π΄ β
(SubRingβ(Poly1ββfld))) |
110 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . 20
β’
(mulGrpβ(Poly1ββfld)) =
(mulGrpβ(Poly1ββfld)) |
111 | 110 | subrgsubm 20251 |
. . . . . . . . . . . . . . . . . . 19
β’ (π΄ β
(SubRingβ(Poly1ββfld)) β π΄ β
(SubMndβ(mulGrpβ(Poly1ββfld)))) |
112 | 109, 111 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β π΄ β
(SubMndβ(mulGrpβ(Poly1ββfld)))) |
113 | 26 | adantl 483 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β π β β0) |
114 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’
(var1ββfld) =
(var1ββfld) |
115 | 114, 101,
57, 58, 59 | subrgvr1cl 21649 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β
(var1ββfld) β π΄) |
116 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . 19
β’
(.gβ(mulGrpβ(Poly1ββfld)))
=
(.gβ(mulGrpβ(Poly1ββfld))) |
117 | 116 | submmulgcl 18926 |
. . . . . . . . . . . . . . . . . 18
β’ ((π΄ β
(SubMndβ(mulGrpβ(Poly1ββfld)))
β§ π β
β0 β§ (var1ββfld) β
π΄) β (π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))
β π΄) |
118 | 112, 113,
115, 117 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))
β π΄) |
119 | | fnfvima 7188 |
. . . . . . . . . . . . . . . . 17
β’ ((πΈ Fn
(Baseβ(Poly1ββfld)) β§ π΄ β
(Baseβ(Poly1ββfld)) β§ (π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))
β π΄) β (πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))
β (πΈ β π΄)) |
120 | 97, 100, 118, 119 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))
β (πΈ β π΄)) |
121 | 108, 120 | sseldd 3950 |
. . . . . . . . . . . . . . 15
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))
β (Baseβ(βfld βs β))) |
122 | 3, 4, 67, 68, 69, 121 | pwselbas 17378 |
. . . . . . . . . . . . . 14
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))):ββΆβ) |
123 | 122 | feqmptd 6915 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))
= (π§ β β β¦ ((πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))βπ§))) |
124 | 52 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β§ π§ β β) β βfld
β CRing) |
125 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β§ π§ β β) β π§ β β) |
126 | 53, 114, 4, 54, 93, 124, 125 | evl1vard 21719 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β§ π§ β β) β
((var1ββfld) β
(Baseβ(Poly1ββfld)) β§ ((πΈβ(var1ββfld))βπ§) = π§)) |
127 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(.gβ(mulGrpββfld)) =
(.gβ(mulGrpββfld)) |
128 | 113 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β§ π§ β β) β π β β0) |
129 | 53, 54, 4, 93, 124, 125, 126, 116, 127, 128 | evl1expd 21727 |
. . . . . . . . . . . . . . . 16
β’ ((((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β§ π§ β β) β ((π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))
β (Baseβ(Poly1ββfld)) β§ ((πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))βπ§) = (π(.gβ(mulGrpββfld))π§))) |
130 | 129 | simprd 497 |
. . . . . . . . . . . . . . 15
β’ ((((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β§ π§ β β) β ((πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))βπ§) = (π(.gβ(mulGrpββfld))π§)) |
131 | | cnfldexp 20846 |
. . . . . . . . . . . . . . . 16
β’ ((π§ β β β§ π β β0)
β (π(.gβ(mulGrpββfld))π§) = (π§βπ)) |
132 | 125, 128,
131 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β§ π§ β β) β (π(.gβ(mulGrpββfld))π§) = (π§βπ)) |
133 | 130, 132 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β§ π§ β β) β ((πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))βπ§) = (π§βπ)) |
134 | 133 | mpteq2dva 5210 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (π§ β β β¦ ((πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))βπ§)) = (π§ β β β¦ (π§βπ))) |
135 | 123, 134 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))
= (π§ β β β¦ (π§βπ))) |
136 | 135, 120 | eqeltrrd 2839 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (π§ β β β¦ (π§βπ)) β (πΈ β π΄)) |
137 | 81 | subrgmcl 20250 |
. . . . . . . . . . 11
β’ (((πΈ β π΄) β
(SubRingβ(βfld βs β)) β§
(β Γ {(πβπ)}) β (πΈ β π΄) β§ (π§ β β β¦ (π§βπ)) β (πΈ β π΄)) β ((β Γ {(πβπ)})(.rβ(βfld
βs β))(π§ β β β¦ (π§βπ))) β (πΈ β π΄)) |
138 | 89, 106, 136, 137 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β ((β Γ {(πβπ)})(.rβ(βfld
βs β))(π§ β β β¦ (π§βπ))) β (πΈ β π΄)) |
139 | 88, 138 | eqeltrrd 2839 |
. . . . . . . . 9
β’ (((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β§ π β (0...π)) β (π§ β β β¦ ((πβπ) Β· (π§βπ))) β (πΈ β π΄)) |
140 | 139 | fmpttd 7068 |
. . . . . . . 8
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (π β (0...π) β¦ (π§ β β β¦ ((πβπ) Β· (π§βπ)))):(0...π)βΆ(πΈ β π΄)) |
141 | 36, 8, 139, 40 | fsuppmptdm 9323 |
. . . . . . . 8
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (π β (0...π) β¦ (π§ β β β¦ ((πβπ) Β· (π§βπ)))) finSupp
(0gβ(βfld βs
β))) |
142 | 5, 51, 8, 66, 140, 141 | gsumsubmcl 19703 |
. . . . . . 7
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β ((βfld βs
β) Ξ£g (π β (0...π) β¦ (π§ β β β¦ ((πβπ) Β· (π§βπ))))) β (πΈ β π΄)) |
143 | 47, 142 | eqeltrrd 2839 |
. . . . . 6
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β (πΈ β π΄)) |
144 | | eleq1 2826 |
. . . . . 6
β’ (π = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β (π β (πΈ β π΄) β (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β (πΈ β π΄))) |
145 | 143, 144 | syl5ibrcom 247 |
. . . . 5
β’ ((π β
(SubRingββfld) β§ (π β β0 β§ π β ((π βͺ {0}) βm
β0))) β (π = (π§ β β β¦ Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β π β (πΈ β π΄))) |
146 | 145 | rexlimdvva 3206 |
. . . 4
β’ (π β
(SubRingββfld) β (βπ β β0 βπ β ((π βͺ {0}) βm
β0)π =
(π§ β β β¦
Ξ£π β (0...π)((πβπ) Β· (π§βπ))) β π β (πΈ β π΄))) |
147 | 2, 146 | syl5 34 |
. . 3
β’ (π β
(SubRingββfld) β (π β (Polyβπ) β π β (πΈ β π΄))) |
148 | | ffun 6676 |
. . . . . 6
β’ (πΈ:(Baseβ(Poly1ββfld))βΆ(Baseβ(βfld
βs β)) β Fun πΈ) |
149 | 95, 148 | ax-mp 5 |
. . . . 5
β’ Fun πΈ |
150 | | fvelima 6913 |
. . . . 5
β’ ((Fun
πΈ β§ π β (πΈ β π΄)) β βπ β π΄ (πΈβπ) = π) |
151 | 149, 150 | mpan 689 |
. . . 4
β’ (π β (πΈ β π΄) β βπ β π΄ (πΈβπ) = π) |
152 | 99 | sselda 3949 |
. . . . . . . . . . 11
β’ ((π β
(SubRingββfld) β§ π β π΄) β π β
(Baseβ(Poly1ββfld))) |
153 | | eqid 2737 |
. . . . . . . . . . . 12
β’ (
Β·π
β(Poly1ββfld)) = (
Β·π
β(Poly1ββfld)) |
154 | | eqid 2737 |
. . . . . . . . . . . 12
β’
(coe1βπ) = (coe1βπ) |
155 | 54, 114, 93, 153, 110, 116, 154 | ply1coe 21683 |
. . . . . . . . . . 11
β’
((βfld β Ring β§ π β
(Baseβ(Poly1ββfld))) β π =
((Poly1ββfld) Ξ£g
(π β
β0 β¦ (((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))))) |
156 | 9, 152, 155 | sylancr 588 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ π β π΄) β π =
((Poly1ββfld) Ξ£g
(π β
β0 β¦ (((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))))) |
157 | 156 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ π β π΄) β (πΈβπ) = (πΈβ((Poly1ββfld)
Ξ£g (π β
β0 β¦ (((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))))) |
158 | | eqid 2737 |
. . . . . . . . . 10
β’
(0gβ(Poly1ββfld)) =
(0gβ(Poly1ββfld)) |
159 | 54 | ply1ring 21635 |
. . . . . . . . . . . 12
β’
(βfld β Ring β
(Poly1ββfld) β Ring) |
160 | 9, 159 | ax-mp 5 |
. . . . . . . . . . 11
β’
(Poly1ββfld) β
Ring |
161 | | ringcmn 20010 |
. . . . . . . . . . 11
β’
((Poly1ββfld) β Ring β
(Poly1ββfld) β CMnd) |
162 | 160, 161 | mp1i 13 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ π β π΄) β
(Poly1ββfld) β CMnd) |
163 | | ringmnd 19981 |
. . . . . . . . . . 11
β’
((βfld βs β) β Ring
β (βfld βs β) β
Mnd) |
164 | 49, 163 | mp1i 13 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ π β π΄) β (βfld
βs β) β Mnd) |
165 | | nn0ex 12426 |
. . . . . . . . . . 11
β’
β0 β V |
166 | 165 | a1i 11 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ π β π΄) β β0 β
V) |
167 | | rhmghm 20166 |
. . . . . . . . . . . 12
β’ (πΈ β
((Poly1ββfld) RingHom (βfld
βs β)) β πΈ β
((Poly1ββfld) GrpHom (βfld
βs β))) |
168 | 56, 167 | ax-mp 5 |
. . . . . . . . . . 11
β’ πΈ β
((Poly1ββfld) GrpHom (βfld
βs β)) |
169 | | ghmmhm 19025 |
. . . . . . . . . . 11
β’ (πΈ β
((Poly1ββfld) GrpHom (βfld
βs β)) β πΈ β
((Poly1ββfld) MndHom (βfld
βs β))) |
170 | 168, 169 | mp1i 13 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ π β π΄) β πΈ β
((Poly1ββfld) MndHom (βfld
βs β))) |
171 | 54 | ply1lmod 21639 |
. . . . . . . . . . . . 13
β’
(βfld β Ring β
(Poly1ββfld) β LMod) |
172 | 9, 171 | mp1i 13 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β
(Poly1ββfld) β LMod) |
173 | 12 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β π β
β) |
174 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
β’
(Baseβπ
) =
(Baseβπ
) |
175 | 154, 59, 58, 174 | coe1f 21598 |
. . . . . . . . . . . . . . . 16
β’ (π β π΄ β (coe1βπ):β0βΆ(Baseβπ
)) |
176 | 57 | subrgbas 20247 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(SubRingββfld) β π = (Baseβπ
)) |
177 | 176 | feq3d 6660 |
. . . . . . . . . . . . . . . 16
β’ (π β
(SubRingββfld) β ((coe1βπ):β0βΆπ β
(coe1βπ):β0βΆ(Baseβπ
))) |
178 | 175, 177 | syl5ibr 246 |
. . . . . . . . . . . . . . 15
β’ (π β
(SubRingββfld) β (π β π΄ β (coe1βπ):β0βΆπ)) |
179 | 178 | imp 408 |
. . . . . . . . . . . . . 14
β’ ((π β
(SubRingββfld) β§ π β π΄) β (coe1βπ):β0βΆπ) |
180 | 179 | ffvelcdmda 7040 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β
((coe1βπ)βπ) β π) |
181 | 173, 180 | sseldd 3950 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β
((coe1βπ)βπ) β β) |
182 | 110, 93 | mgpbas 19909 |
. . . . . . . . . . . . 13
β’
(Baseβ(Poly1ββfld)) =
(Baseβ(mulGrpβ(Poly1ββfld))) |
183 | 110 | ringmgp 19977 |
. . . . . . . . . . . . . 14
β’
((Poly1ββfld) β Ring β
(mulGrpβ(Poly1ββfld)) β
Mnd) |
184 | 160, 183 | mp1i 13 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β
(mulGrpβ(Poly1ββfld)) β
Mnd) |
185 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β π β
β0) |
186 | 114, 54, 93 | vr1cl 21604 |
. . . . . . . . . . . . . 14
β’
(βfld β Ring β
(var1ββfld) β
(Baseβ(Poly1ββfld))) |
187 | 9, 186 | mp1i 13 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β
(var1ββfld) β
(Baseβ(Poly1ββfld))) |
188 | 182, 116,
184, 185, 187 | mulgnn0cld 18904 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β (π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))
β (Baseβ(Poly1ββfld))) |
189 | 54 | ply1sca 21640 |
. . . . . . . . . . . . . 14
β’
(βfld β Ring β βfld =
(Scalarβ(Poly1ββfld))) |
190 | 9, 189 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
βfld =
(Scalarβ(Poly1ββfld)) |
191 | 93, 190, 153, 4 | lmodvscl 20355 |
. . . . . . . . . . . 12
β’
(((Poly1ββfld) β LMod β§
((coe1βπ)βπ) β β β§ (π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))
β (Baseβ(Poly1ββfld))) β (((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))
β (Baseβ(Poly1ββfld))) |
192 | 172, 181,
188, 191 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β
(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))
β (Baseβ(Poly1ββfld))) |
193 | 192 | fmpttd 7068 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ π β π΄) β (π β β0 β¦
(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))):β0βΆ(Baseβ(Poly1ββfld))) |
194 | 165 | mptex 7178 |
. . . . . . . . . . . . 13
β’ (π β β0
β¦ (((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
β V |
195 | | funmpt 6544 |
. . . . . . . . . . . . 13
β’ Fun
(π β
β0 β¦ (((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))) |
196 | | fvex 6860 |
. . . . . . . . . . . . 13
β’
(0gβ(Poly1ββfld))
β V |
197 | 194, 195,
196 | 3pm3.2i 1340 |
. . . . . . . . . . . 12
β’ ((π β β0
β¦ (((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
β V β§ Fun (π β β0 β¦ (((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
β§ (0gβ(Poly1ββfld)) β V) |
198 | 197 | a1i 11 |
. . . . . . . . . . 11
β’ ((π β
(SubRingββfld) β§ π β π΄) β ((π β β0 β¦
(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
β V β§ Fun (π β β0 β¦ (((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
β§ (0gβ(Poly1ββfld)) β V)) |
199 | 154, 93, 54, 17 | coe1sfi 21600 |
. . . . . . . . . . . . 13
β’ (π β
(Baseβ(Poly1ββfld)) β
(coe1βπ)
finSupp 0) |
200 | 152, 199 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β
(SubRingββfld) β§ π β π΄) β (coe1βπ) finSupp 0) |
201 | 200 | fsuppimpd 9319 |
. . . . . . . . . . 11
β’ ((π β
(SubRingββfld) β§ π β π΄) β ((coe1βπ) supp 0) β
Fin) |
202 | 179 | feqmptd 6915 |
. . . . . . . . . . . . . 14
β’ ((π β
(SubRingββfld) β§ π β π΄) β (coe1βπ) = (π β β0 β¦
((coe1βπ)βπ))) |
203 | 202 | oveq1d 7377 |
. . . . . . . . . . . . 13
β’ ((π β
(SubRingββfld) β§ π β π΄) β ((coe1βπ) supp 0) = ((π β β0 β¦
((coe1βπ)βπ)) supp 0)) |
204 | | eqimss2 4006 |
. . . . . . . . . . . . 13
β’
(((coe1βπ) supp 0) = ((π β β0 β¦
((coe1βπ)βπ)) supp 0) β ((π β β0 β¦
((coe1βπ)βπ)) supp 0) β
((coe1βπ)
supp 0)) |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β
(SubRingββfld) β§ π β π΄) β ((π β β0 β¦
((coe1βπ)βπ)) supp 0) β
((coe1βπ)
supp 0)) |
206 | 9, 171 | mp1i 13 |
. . . . . . . . . . . . 13
β’ ((π β
(SubRingββfld) β§ π β π΄) β
(Poly1ββfld) β LMod) |
207 | 93, 190, 153, 17, 158 | lmod0vs 20371 |
. . . . . . . . . . . . 13
β’
(((Poly1ββfld) β LMod β§ π₯ β
(Baseβ(Poly1ββfld))) β (0(
Β·π
β(Poly1ββfld))π₯) =
(0gβ(Poly1ββfld))) |
208 | 206, 207 | sylan 581 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π₯ β
(Baseβ(Poly1ββfld))) β (0(
Β·π
β(Poly1ββfld))π₯) =
(0gβ(Poly1ββfld))) |
209 | | c0ex 11156 |
. . . . . . . . . . . . 13
β’ 0 β
V |
210 | 209 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β
(SubRingββfld) β§ π β π΄) β 0 β V) |
211 | 205, 208,
180, 188, 210 | suppssov1 8134 |
. . . . . . . . . . 11
β’ ((π β
(SubRingββfld) β§ π β π΄) β ((π β β0 β¦
(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
supp (0gβ(Poly1ββfld))) β ((coe1βπ)
supp 0)) |
212 | | suppssfifsupp 9327 |
. . . . . . . . . . 11
β’ ((((π β β0
β¦ (((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
β V β§ Fun (π β β0 β¦ (((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
β§ (0gβ(Poly1ββfld)) β V) β§ (((coe1βπ) supp 0) β Fin β§ ((π β β0 β¦
(((coe1βπ)βπ)(
Β·π β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
supp (0gβ(Poly1ββfld))) β ((coe1βπ)
supp 0))) β (π β β0 β¦ (((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
finSupp (0gβ(Poly1ββfld))) |
213 | 198, 201,
211, 212 | syl12anc 836 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ π β π΄) β (π β β0 β¦
(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
finSupp (0gβ(Poly1ββfld))) |
214 | 93, 158, 162, 164, 166, 170, 193, 213 | gsummhm 19722 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ π β π΄) β ((βfld
βs β) Ξ£g (πΈ β (π β β0 β¦
(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))))
= (πΈβ((Poly1ββfld) Ξ£g (π β β0 β¦ (((coe1βπ)βπ)( Β·π β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))))) |
215 | 95 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β
(SubRingββfld) β§ π β π΄) β πΈ:(Baseβ(Poly1ββfld))βΆ(Baseβ(βfld
βs β))) |
216 | 215, 192 | cofmpt 7083 |
. . . . . . . . . . 11
β’ ((π β
(SubRingββfld) β§ π β π΄) β (πΈ β (π β β0 β¦
(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))))
= (π β β0 β¦ (πΈβ(((coe1βπ)βπ)( Β·π β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))))) |
217 | 9 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β
βfld β Ring) |
218 | 6 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β β
β V) |
219 | 95 | ffvelcdmi 7039 |
. . . . . . . . . . . . . . . 16
β’
((((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))
β (Baseβ(Poly1ββfld)) β (πΈβ(((coe1βπ)βπ)( Β·π β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
β (Baseβ(βfld βs β))) |
220 | 192, 219 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β (πΈβ(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
β (Baseβ(βfld βs β))) |
221 | 3, 4, 67, 217, 218, 220 | pwselbas 17378 |
. . . . . . . . . . . . . 14
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β (πΈβ(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))):ββΆβ) |
222 | 221 | feqmptd 6915 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β (πΈβ(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
= (π§ β β β¦ ((πΈβ(((coe1βπ)βπ)( Β·π β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))βπ§))) |
223 | 52 | a1i 11 |
. . . . . . . . . . . . . . . 16
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β§ π§ β β) β
βfld β CRing) |
224 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β§ π§ β β) β π§ β
β) |
225 | 53, 114, 4, 54, 93, 223, 224 | evl1vard 21719 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β§ π§ β β) β
((var1ββfld) β
(Baseβ(Poly1ββfld)) β§ ((πΈβ(var1ββfld))βπ§) = π§)) |
226 | 185 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β§ π§ β β) β π β
β0) |
227 | 53, 54, 4, 93, 223, 224, 225, 116, 127, 226 | evl1expd 21727 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β§ π§ β β) β ((π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))
β (Baseβ(Poly1ββfld)) β§ ((πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))βπ§) = (π(.gβ(mulGrpββfld))π§))) |
228 | 224, 226,
131 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β§ π§ β β) β (π(.gβ(mulGrpββfld))π§) = (π§βπ)) |
229 | 228 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β§ π§ β β) β (((πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))βπ§) = (π(.gβ(mulGrpββfld))π§) β ((πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))βπ§) = (π§βπ))) |
230 | 229 | anbi2d 630 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β§ π§ β β) β (((π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))
β (Baseβ(Poly1ββfld)) β§ ((πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))βπ§) = (π(.gβ(mulGrpββfld))π§)) β ((π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)) β
(Baseβ(Poly1ββfld)) β§ ((πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))βπ§) = (π§βπ)))) |
231 | 227, 230 | mpbid 231 |
. . . . . . . . . . . . . . . 16
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β§ π§ β β) β ((π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))
β (Baseβ(Poly1ββfld)) β§ ((πΈβ(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))βπ§) = (π§βπ))) |
232 | 181 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β§ π§ β β) β
((coe1βπ)βπ) β β) |
233 | 53, 54, 4, 93, 223, 224, 231, 232, 153, 80 | evl1vsd 21726 |
. . . . . . . . . . . . . . 15
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β§ π§ β β) β
((((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))
β (Baseβ(Poly1ββfld)) β§ ((πΈβ(((coe1βπ)βπ)( Β·π β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))βπ§) = (((coe1βπ)βπ) Β· (π§βπ)))) |
234 | 233 | simprd 497 |
. . . . . . . . . . . . . 14
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β§ π§ β β) β ((πΈβ(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))βπ§) = (((coe1βπ)βπ) Β· (π§βπ))) |
235 | 234 | mpteq2dva 5210 |
. . . . . . . . . . . . 13
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β (π§ β β β¦ ((πΈβ(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))βπ§)) = (π§ β β β¦ (((coe1βπ)βπ) Β· (π§βπ)))) |
236 | 222, 235 | eqtrd 2777 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β β0) β (πΈβ(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))
= (π§ β β β¦ (((coe1βπ)βπ) Β· (π§βπ)))) |
237 | 236 | mpteq2dva 5210 |
. . . . . . . . . . 11
β’ ((π β
(SubRingββfld) β§ π β π΄) β (π β β0 β¦ (πΈβ(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))))
= (π β β0 β¦ (π§ β β
β¦ (((coe1βπ)βπ) Β· (π§βπ))))) |
238 | 216, 237 | eqtrd 2777 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ π β π΄) β (πΈ β (π β β0 β¦
(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld)))))
= (π β β0 β¦ (π§ β β
β¦ (((coe1βπ)βπ) Β· (π§βπ))))) |
239 | 238 | oveq2d 7378 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ π β π΄) β ((βfld
βs β) Ξ£g (πΈ β (π β β0 β¦
(((coe1βπ)βπ)( Β·π
β(Poly1ββfld))(π(.gβ(mulGrpβ(Poly1ββfld)))(var1ββfld))))))
= ((βfld βs β) Ξ£g (π β
β0 β¦ (π§ β β β¦ (((coe1βπ)βπ) Β· (π§βπ)))))) |
240 | 157, 214,
239 | 3eqtr2d 2783 |
. . . . . . . 8
β’ ((π β
(SubRingββfld) β§ π β π΄) β (πΈβπ) = ((βfld
βs β) Ξ£g (π β β0
β¦ (π§ β β
β¦ (((coe1βπ)βπ) Β· (π§βπ)))))) |
241 | 6 | a1i 11 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ π β π΄) β β β V) |
242 | 9, 10 | mp1i 13 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ π β π΄) β βfld β
CMnd) |
243 | 181 | adantlr 714 |
. . . . . . . . . . 11
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β β0) β
((coe1βπ)βπ) β β) |
244 | 33 | adantll 713 |
. . . . . . . . . . 11
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β β0) β (π§βπ) β β) |
245 | 243, 244 | mulcld 11182 |
. . . . . . . . . 10
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β β0) β
(((coe1βπ)βπ) Β· (π§βπ)) β β) |
246 | 245 | anasss 468 |
. . . . . . . . 9
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ (π§ β β β§ π β β0)) β
(((coe1βπ)βπ) Β· (π§βπ)) β β) |
247 | 165 | mptex 7178 |
. . . . . . . . . . . 12
β’ (π β β0
β¦ (π§ β β
β¦ (((coe1βπ)βπ) Β· (π§βπ)))) β V |
248 | | funmpt 6544 |
. . . . . . . . . . . 12
β’ Fun
(π β
β0 β¦ (π§ β β β¦
(((coe1βπ)βπ) Β· (π§βπ)))) |
249 | 247, 248,
39 | 3pm3.2i 1340 |
. . . . . . . . . . 11
β’ ((π β β0
β¦ (π§ β β
β¦ (((coe1βπ)βπ) Β· (π§βπ)))) β V β§ Fun (π β β0 β¦ (π§ β β β¦
(((coe1βπ)βπ) Β· (π§βπ)))) β§
(0gβ(βfld βs β))
β V) |
250 | 249 | a1i 11 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ π β π΄) β ((π β β0 β¦ (π§ β β β¦
(((coe1βπ)βπ) Β· (π§βπ)))) β V β§ Fun (π β β0 β¦ (π§ β β β¦
(((coe1βπ)βπ) Β· (π§βπ)))) β§
(0gβ(βfld βs β))
β V)) |
251 | | fzfid 13885 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ π β π΄) β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) β Fin) |
252 | | eldifn 4092 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (β0
β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))) β Β¬ π β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))) |
253 | 252 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β Β¬ π β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))) |
254 | 152 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β π β
(Baseβ(Poly1ββfld))) |
255 | | eldifi 4091 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β (β0
β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))) β π β β0) |
256 | 255 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β π β β0) |
257 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (
deg1 ββfld) = ( deg1
ββfld) |
258 | 257, 54, 93, 17, 154 | deg1ge 25479 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β
(Baseβ(Poly1ββfld)) β§ π β β0
β§ ((coe1βπ)βπ) β 0) β π β€ (( deg1
ββfld)βπ)) |
259 | 258 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β
(Baseβ(Poly1ββfld)) β§ π β β0)
β (((coe1βπ)βπ) β 0 β π β€ (( deg1
ββfld)βπ))) |
260 | 254, 256,
259 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β
(((coe1βπ)βπ) β 0 β π β€ (( deg1
ββfld)βπ))) |
261 | | 0xr 11209 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 0 β
β* |
262 | 257, 54, 93 | deg1xrcl 25463 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β
(Baseβ(Poly1ββfld)) β ((
deg1 ββfld)βπ) β
β*) |
263 | 152, 262 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β
(SubRingββfld) β§ π β π΄) β (( deg1
ββfld)βπ) β
β*) |
264 | 263 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β (( deg1
ββfld)βπ) β
β*) |
265 | | xrmax2 13102 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((0
β β* β§ (( deg1
ββfld)βπ) β β*) β ((
deg1 ββfld)βπ) β€ if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) |
266 | 261, 264,
265 | sylancr 588 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β (( deg1
ββfld)βπ) β€ if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) |
267 | 256 | nn0red 12481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β π β β) |
268 | 267 | rexrd 11212 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β π β β*) |
269 | | ifcl 4536 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((
deg1 ββfld)βπ) β β* β§ 0 β
β*) β if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0) β
β*) |
270 | 264, 261,
269 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0) β
β*) |
271 | | xrletr 13084 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β*
β§ (( deg1 ββfld)βπ) β β* β§ if(0 β€
(( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0) β β*) β
((π β€ (( deg1
ββfld)βπ) β§ (( deg1
ββfld)βπ) β€ if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) β π β€ if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))) |
272 | 268, 264,
270, 271 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β ((π β€ (( deg1
ββfld)βπ) β§ (( deg1
ββfld)βπ) β€ if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) β π β€ if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))) |
273 | 266, 272 | mpan2d 693 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β (π β€ (( deg1
ββfld)βπ) β π β€ if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))) |
274 | 260, 273 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β
(((coe1βπ)βπ) β 0 β π β€ if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))) |
275 | 274, 256 | jctild 527 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β
(((coe1βπ)βπ) β 0 β (π β β0 β§ π β€ if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) |
276 | 257, 54, 93 | deg1cl 25464 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β
(Baseβ(Poly1ββfld)) β ((
deg1 ββfld)βπ) β (β0 βͺ
{-β})) |
277 | 152, 276 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β
(SubRingββfld) β§ π β π΄) β (( deg1
ββfld)βπ) β (β0 βͺ
{-β})) |
278 | | elun 4113 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((
deg1 ββfld)βπ) β (β0 βͺ
{-β}) β ((( deg1
ββfld)βπ) β β0 β¨ ((
deg1 ββfld)βπ) β {-β})) |
279 | 277, 278 | sylib 217 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β
(SubRingββfld) β§ π β π΄) β ((( deg1
ββfld)βπ) β β0 β¨ ((
deg1 ββfld)βπ) β {-β})) |
280 | | nn0ge0 12445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((
deg1 ββfld)βπ) β β0 β 0 β€ ((
deg1 ββfld)βπ)) |
281 | 280 | iftrued 4499 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((
deg1 ββfld)βπ) β β0 β if(0 β€
(( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0) = (( deg1
ββfld)βπ)) |
282 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((
deg1 ββfld)βπ) β β0 β ((
deg1 ββfld)βπ) β
β0) |
283 | 281, 282 | eqeltrd 2838 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((
deg1 ββfld)βπ) β β0 β if(0 β€
(( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0) β
β0) |
284 | | mnflt0 13053 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ -β
< 0 |
285 | | mnfxr 11219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ -β
β β* |
286 | | xrltnle 11229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’
((-β β β* β§ 0 β
β*) β (-β < 0 β Β¬ 0 β€
-β)) |
287 | 285, 261,
286 | mp2an 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (-β
< 0 β Β¬ 0 β€ -β) |
288 | 284, 287 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ Β¬ 0
β€ -β |
289 | | elsni 4608 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (((
deg1 ββfld)βπ) β {-β} β (( deg1
ββfld)βπ) = -β) |
290 | 289 | breq2d 5122 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (((
deg1 ββfld)βπ) β {-β} β (0 β€ ((
deg1 ββfld)βπ) β 0 β€ -β)) |
291 | 288, 290 | mtbiri 327 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((
deg1 ββfld)βπ) β {-β} β Β¬ 0 β€ ((
deg1 ββfld)βπ)) |
292 | 291 | iffalsed 4502 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((
deg1 ββfld)βπ) β {-β} β if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0) = 0) |
293 | | 0nn0 12435 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ 0 β
β0 |
294 | 292, 293 | eqeltrdi 2846 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((
deg1 ββfld)βπ) β {-β} β if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0) β
β0) |
295 | 283, 294 | jaoi 856 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((((
deg1 ββfld)βπ) β β0 β¨ ((
deg1 ββfld)βπ) β {-β}) β if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0) β
β0) |
296 | 279, 295 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β
(SubRingββfld) β§ π β π΄) β if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0) β
β0) |
297 | 296 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0) β
β0) |
298 | | fznn0 13540 |
. . . . . . . . . . . . . . . . . . . 20
β’ (if(0
β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0) β β0 β
(π β (0...if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)) β (π β β0 β§ π β€ if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) |
299 | 297, 298 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β (π β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) β (π β β0 β§ π β€ if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) |
300 | 275, 299 | sylibrd 259 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β
(((coe1βπ)βπ) β 0 β π β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)))) |
301 | 300 | necon1bd 2962 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β (Β¬ π β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) β ((coe1βπ)βπ) = 0)) |
302 | 253, 301 | mpd 15 |
. . . . . . . . . . . . . . . 16
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β ((coe1βπ)βπ) = 0) |
303 | 302 | oveq1d 7377 |
. . . . . . . . . . . . . . 15
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β
(((coe1βπ)βπ) Β· (π§βπ)) = (0 Β· (π§βπ))) |
304 | 255, 244 | sylan2 594 |
. . . . . . . . . . . . . . . 16
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β (π§βπ) β β) |
305 | 304 | mul02d 11360 |
. . . . . . . . . . . . . . 15
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β (0 Β· (π§βπ)) = 0) |
306 | 303, 305 | eqtrd 2777 |
. . . . . . . . . . . . . 14
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β
(((coe1βπ)βπ) Β· (π§βπ)) = 0) |
307 | 306 | an32s 651 |
. . . . . . . . . . . . 13
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β§ π§ β β) β
(((coe1βπ)βπ) Β· (π§βπ)) = 0) |
308 | 307 | mpteq2dva 5210 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β (π§ β β β¦
(((coe1βπ)βπ) Β· (π§βπ))) = (π§ β β β¦ 0)) |
309 | | fconstmpt 5699 |
. . . . . . . . . . . . 13
β’ (β
Γ {0}) = (π§ β
β β¦ 0) |
310 | | ringmnd 19981 |
. . . . . . . . . . . . . . 15
β’
(βfld β Ring β βfld β
Mnd) |
311 | 9, 310 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’
βfld β Mnd |
312 | 3, 17 | pws0g 18599 |
. . . . . . . . . . . . . 14
β’
((βfld β Mnd β§ β β V) β
(β Γ {0}) = (0gβ(βfld
βs β))) |
313 | 311, 6, 312 | mp2an 691 |
. . . . . . . . . . . . 13
β’ (β
Γ {0}) = (0gβ(βfld
βs β)) |
314 | 309, 313 | eqtr3i 2767 |
. . . . . . . . . . . 12
β’ (π§ β β β¦ 0) =
(0gβ(βfld βs
β)) |
315 | 308, 314 | eqtrdi 2793 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π β (β0 β
(0...if(0 β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β (π§ β β β¦
(((coe1βπ)βπ) Β· (π§βπ))) =
(0gβ(βfld βs
β))) |
316 | 315, 166 | suppss2 8136 |
. . . . . . . . . 10
β’ ((π β
(SubRingββfld) β§ π β π΄) β ((π β β0 β¦ (π§ β β β¦
(((coe1βπ)βπ) Β· (π§βπ)))) supp
(0gβ(βfld βs
β))) β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))) |
317 | | suppssfifsupp 9327 |
. . . . . . . . . 10
β’ ((((π β β0
β¦ (π§ β β
β¦ (((coe1βπ)βπ) Β· (π§βπ)))) β V β§ Fun (π β β0 β¦ (π§ β β β¦
(((coe1βπ)βπ) Β· (π§βπ)))) β§
(0gβ(βfld βs β))
β V) β§ ((0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) β Fin β§ ((π β β0 β¦ (π§ β β β¦
(((coe1βπ)βπ) Β· (π§βπ)))) supp
(0gβ(βfld βs
β))) β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β (π β β0 β¦ (π§ β β β¦
(((coe1βπ)βπ) Β· (π§βπ)))) finSupp
(0gβ(βfld βs
β))) |
318 | 250, 251,
316, 317 | syl12anc 836 |
. . . . . . . . 9
β’ ((π β
(SubRingββfld) β§ π β π΄) β (π β β0 β¦ (π§ β β β¦
(((coe1βπ)βπ) Β· (π§βπ)))) finSupp
(0gβ(βfld βs
β))) |
319 | 3, 4, 5, 241, 166, 242, 246, 318 | pwsgsum 19766 |
. . . . . . . 8
β’ ((π β
(SubRingββfld) β§ π β π΄) β ((βfld
βs β) Ξ£g (π β β0
β¦ (π§ β β
β¦ (((coe1βπ)βπ) Β· (π§βπ))))) = (π§ β β β¦
(βfld Ξ£g (π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ)))))) |
320 | | fz0ssnn0 13543 |
. . . . . . . . . . . 12
β’ (0...if(0
β€ (( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)) β
β0 |
321 | | resmpt 5996 |
. . . . . . . . . . . 12
β’
((0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) β β0 β
((π β
β0 β¦ (((coe1βπ)βπ) Β· (π§βπ))) βΎ (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))) = (π β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) β¦ (((coe1βπ)βπ) Β· (π§βπ)))) |
322 | 320, 321 | ax-mp 5 |
. . . . . . . . . . 11
β’ ((π β β0
β¦ (((coe1βπ)βπ) Β· (π§βπ))) βΎ (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))) = (π β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) β¦ (((coe1βπ)βπ) Β· (π§βπ))) |
323 | 322 | oveq2i 7373 |
. . . . . . . . . 10
β’
(βfld Ξ£g ((π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))) βΎ (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)))) = (βfld
Ξ£g (π β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) β¦ (((coe1βπ)βπ) Β· (π§βπ)))) |
324 | 9, 10 | mp1i 13 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β βfld
β CMnd) |
325 | 165 | a1i 11 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β β0
β V) |
326 | 245 | fmpttd 7068 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β (π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))):β0βΆβ) |
327 | 306, 325 | suppss2 8136 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β ((π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))) supp 0) β (0...if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0))) |
328 | 165 | mptex 7178 |
. . . . . . . . . . . . . 14
β’ (π β β0
β¦ (((coe1βπ)βπ) Β· (π§βπ))) β V |
329 | | funmpt 6544 |
. . . . . . . . . . . . . 14
β’ Fun
(π β
β0 β¦ (((coe1βπ)βπ) Β· (π§βπ))) |
330 | 328, 329,
209 | 3pm3.2i 1340 |
. . . . . . . . . . . . 13
β’ ((π β β0
β¦ (((coe1βπ)βπ) Β· (π§βπ))) β V β§ Fun (π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))) β§ 0 β V) |
331 | 330 | a1i 11 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β ((π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))) β V β§ Fun (π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))) β§ 0 β V)) |
332 | | fzfid 13885 |
. . . . . . . . . . . 12
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β (0...if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)) β Fin) |
333 | | suppssfifsupp 9327 |
. . . . . . . . . . . 12
β’ ((((π β β0
β¦ (((coe1βπ)βπ) Β· (π§βπ))) β V β§ Fun (π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))) β§ 0 β V) β§ ((0...if(0 β€
(( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)) β Fin β§ ((π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))) supp 0) β (0...if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)))) β (π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))) finSupp 0) |
334 | 331, 332,
327, 333 | syl12anc 836 |
. . . . . . . . . . 11
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β (π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))) finSupp 0) |
335 | 4, 17, 324, 325, 326, 327, 334 | gsumres 19697 |
. . . . . . . . . 10
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β
(βfld Ξ£g ((π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))) βΎ (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)))) = (βfld
Ξ£g (π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))))) |
336 | | elfznn0 13541 |
. . . . . . . . . . . 12
β’ (π β (0...if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0)) β π β β0) |
337 | 336, 245 | sylan2 594 |
. . . . . . . . . . 11
β’ ((((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β§ π β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))) β (((coe1βπ)βπ) Β· (π§βπ)) β β) |
338 | 332, 337 | gsumfsum 20880 |
. . . . . . . . . 10
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β
(βfld Ξ£g (π β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0)) β¦ (((coe1βπ)βπ) Β· (π§βπ)))) = Ξ£π β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))(((coe1βπ)βπ) Β· (π§βπ))) |
339 | 323, 335,
338 | 3eqtr3a 2801 |
. . . . . . . . 9
β’ (((π β
(SubRingββfld) β§ π β π΄) β§ π§ β β) β
(βfld Ξ£g (π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ)))) = Ξ£π β (0...if(0 β€ (( deg1
ββfld)βπ), (( deg1
ββfld)βπ), 0))(((coe1βπ)βπ) Β· (π§βπ))) |
340 | 339 | mpteq2dva 5210 |
. . . . . . . 8
β’ ((π β
(SubRingββfld) β§ π β π΄) β (π§ β β β¦
(βfld Ξ£g (π β β0 β¦
(((coe1βπ)βπ) Β· (π§βπ))))) = (π§ β β β¦ Ξ£π β (0...if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0))(((coe1βπ)βπ) Β· (π§βπ)))) |
341 | 240, 319,
340 | 3eqtrd 2781 |
. . . . . . 7
β’ ((π β
(SubRingββfld) β§ π β π΄) β (πΈβπ) = (π§ β β β¦ Ξ£π β (0...if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0))(((coe1βπ)βπ) Β· (π§βπ)))) |
342 | 12 | adantr 482 |
. . . . . . . 8
β’ ((π β
(SubRingββfld) β§ π β π΄) β π β β) |
343 | | elplyr 25578 |
. . . . . . . 8
β’ ((π β β β§ if(0 β€
(( deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0) β β0 β§
(coe1βπ):β0βΆπ) β (π§ β β β¦ Ξ£π β (0...if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0))(((coe1βπ)βπ) Β· (π§βπ))) β (Polyβπ)) |
344 | 342, 296,
179, 343 | syl3anc 1372 |
. . . . . . 7
β’ ((π β
(SubRingββfld) β§ π β π΄) β (π§ β β β¦ Ξ£π β (0...if(0 β€ ((
deg1 ββfld)βπ), (( deg1
ββfld)βπ), 0))(((coe1βπ)βπ) Β· (π§βπ))) β (Polyβπ)) |
345 | 341, 344 | eqeltrd 2838 |
. . . . . 6
β’ ((π β
(SubRingββfld) β§ π β π΄) β (πΈβπ) β (Polyβπ)) |
346 | | eleq1 2826 |
. . . . . 6
β’ ((πΈβπ) = π β ((πΈβπ) β (Polyβπ) β π β (Polyβπ))) |
347 | 345, 346 | syl5ibcom 244 |
. . . . 5
β’ ((π β
(SubRingββfld) β§ π β π΄) β ((πΈβπ) = π β π β (Polyβπ))) |
348 | 347 | rexlimdva 3153 |
. . . 4
β’ (π β
(SubRingββfld) β (βπ β π΄ (πΈβπ) = π β π β (Polyβπ))) |
349 | 151, 348 | syl5 34 |
. . 3
β’ (π β
(SubRingββfld) β (π β (πΈ β π΄) β π β (Polyβπ))) |
350 | 147, 349 | impbid 211 |
. 2
β’ (π β
(SubRingββfld) β (π β (Polyβπ) β π β (πΈ β π΄))) |
351 | 350 | eqrdv 2735 |
1
β’ (π β
(SubRingββfld) β (Polyβπ) = (πΈ β π΄)) |