Step | Hyp | Ref
| Expression |
1 | | simpl 482 |
. . . 4
β’ ((π β§ π₯ β π) β π) |
2 | | elirng.s |
. . . . . 6
β’ (π β π β (SubRingβπ
)) |
3 | | irngval.b |
. . . . . . 7
β’ π΅ = (Baseβπ
) |
4 | 3 | subrgss 20470 |
. . . . . 6
β’ (π β (SubRingβπ
) β π β π΅) |
5 | 2, 4 | syl 17 |
. . . . 5
β’ (π β π β π΅) |
6 | 5 | sselda 3982 |
. . . 4
β’ ((π β§ π₯ β π) β π₯ β π΅) |
7 | | eqid 2731 |
. . . . . . . . . 10
β’
(Poly1βπ
) = (Poly1βπ
) |
8 | | irngval.u |
. . . . . . . . . 10
β’ π = (π
βΎs π) |
9 | | eqid 2731 |
. . . . . . . . . 10
β’
(Poly1βπ) = (Poly1βπ) |
10 | | eqid 2731 |
. . . . . . . . . 10
β’
(Baseβ(Poly1βπ)) =
(Baseβ(Poly1βπ)) |
11 | 2 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β π β (SubRingβπ
)) |
12 | | eqid 2731 |
. . . . . . . . . 10
β’
((Poly1βπ
) βΎs
(Baseβ(Poly1βπ))) = ((Poly1βπ
) βΎs
(Baseβ(Poly1βπ))) |
13 | | eqid 2731 |
. . . . . . . . . . 11
β’
(var1βπ
) = (var1βπ
) |
14 | 13, 11, 8, 9, 10 | subrgvr1cl 22104 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (var1βπ
) β
(Baseβ(Poly1βπ))) |
15 | | eqid 2731 |
. . . . . . . . . . 11
β’
(algScβ(Poly1βπ
)) =
(algScβ(Poly1βπ
)) |
16 | | simpr 484 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β π₯ β π) |
17 | 15, 8, 7, 9, 10, 11, 16 | asclply1subcl 33101 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β
((algScβ(Poly1βπ
))βπ₯) β
(Baseβ(Poly1βπ))) |
18 | 7, 8, 9, 10, 11, 12, 14, 17 | ressply1sub 33100 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β ((var1βπ
)(-gβ(Poly1βπ))((algScβ(Poly1βπ
))βπ₯)) = ((var1βπ
)(-gβ((Poly1βπ
) βΎs
(Baseβ(Poly1βπ))))((algScβ(Poly1βπ
))βπ₯))) |
19 | 7, 8, 9, 10 | subrgply1 22075 |
. . . . . . . . . . . 12
β’ (π β (SubRingβπ
) β
(Baseβ(Poly1βπ)) β
(SubRingβ(Poly1βπ
))) |
20 | | subrgsubg 20475 |
. . . . . . . . . . . 12
β’
((Baseβ(Poly1βπ)) β
(SubRingβ(Poly1βπ
)) β
(Baseβ(Poly1βπ)) β
(SubGrpβ(Poly1βπ
))) |
21 | 2, 19, 20 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β
(Baseβ(Poly1βπ)) β
(SubGrpβ(Poly1βπ
))) |
22 | 21 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β
(Baseβ(Poly1βπ)) β
(SubGrpβ(Poly1βπ
))) |
23 | | eqid 2731 |
. . . . . . . . . . 11
β’
(-gβ(Poly1βπ
)) =
(-gβ(Poly1βπ
)) |
24 | | eqid 2731 |
. . . . . . . . . . 11
β’
(-gβ((Poly1βπ
) βΎs
(Baseβ(Poly1βπ)))) =
(-gβ((Poly1βπ
) βΎs
(Baseβ(Poly1βπ)))) |
25 | 23, 12, 24 | subgsub 19061 |
. . . . . . . . . 10
β’
(((Baseβ(Poly1βπ)) β
(SubGrpβ(Poly1βπ
)) β§ (var1βπ
) β
(Baseβ(Poly1βπ)) β§
((algScβ(Poly1βπ
))βπ₯) β
(Baseβ(Poly1βπ))) β ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) = ((var1βπ
)(-gβ((Poly1βπ
) βΎs
(Baseβ(Poly1βπ))))((algScβ(Poly1βπ
))βπ₯))) |
26 | 22, 14, 17, 25 | syl3anc 1370 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) = ((var1βπ
)(-gβ((Poly1βπ
) βΎs
(Baseβ(Poly1βπ))))((algScβ(Poly1βπ
))βπ₯))) |
27 | 18, 26 | eqtr4d 2774 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β ((var1βπ
)(-gβ(Poly1βπ))((algScβ(Poly1βπ
))βπ₯)) = ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) |
28 | | elirng.r |
. . . . . . . . . . . . 13
β’ (π β π
β CRing) |
29 | 8 | subrgcrng 20473 |
. . . . . . . . . . . . 13
β’ ((π
β CRing β§ π β (SubRingβπ
)) β π β CRing) |
30 | 28, 2, 29 | syl2anc 583 |
. . . . . . . . . . . 12
β’ (π β π β CRing) |
31 | 9 | ply1crng 22041 |
. . . . . . . . . . . 12
β’ (π β CRing β
(Poly1βπ)
β CRing) |
32 | 30, 31 | syl 17 |
. . . . . . . . . . 11
β’ (π β
(Poly1βπ)
β CRing) |
33 | 32 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (Poly1βπ) β CRing) |
34 | 33 | crnggrpd 20148 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β (Poly1βπ) β Grp) |
35 | | eqid 2731 |
. . . . . . . . . 10
β’
(-gβ(Poly1βπ)) =
(-gβ(Poly1βπ)) |
36 | 10, 35 | grpsubcl 18946 |
. . . . . . . . 9
β’
(((Poly1βπ) β Grp β§
(var1βπ
)
β (Baseβ(Poly1βπ)) β§
((algScβ(Poly1βπ
))βπ₯) β
(Baseβ(Poly1βπ))) β ((var1βπ
)(-gβ(Poly1βπ))((algScβ(Poly1βπ
))βπ₯)) β (Baseβ(Poly1βπ))) |
37 | 34, 14, 17, 36 | syl3anc 1370 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β ((var1βπ
)(-gβ(Poly1βπ))((algScβ(Poly1βπ
))βπ₯)) β (Baseβ(Poly1βπ))) |
38 | 27, 37 | eqeltrrd 2833 |
. . . . . . 7
β’ ((π β§ π₯ β π) β ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) β (Baseβ(Poly1βπ))) |
39 | | eqid 2731 |
. . . . . . . . 9
β’
(Baseβ(Poly1βπ
)) =
(Baseβ(Poly1βπ
)) |
40 | | eqid 2731 |
. . . . . . . . 9
β’
((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) = ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) |
41 | | eqid 2731 |
. . . . . . . . 9
β’
(eval1βπ
) = (eval1βπ
) |
42 | | irngss.1 |
. . . . . . . . . 10
β’ (π β π
β NzRing) |
43 | 42 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π
β NzRing) |
44 | 28 | adantr 480 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π
β CRing) |
45 | | eqid 2731 |
. . . . . . . . 9
β’
(Monic1pβπ
) = (Monic1pβπ
) |
46 | | eqid 2731 |
. . . . . . . . 9
β’ (
deg1 βπ
) =
( deg1 βπ
) |
47 | | irngval.0 |
. . . . . . . . 9
β’ 0 =
(0gβπ
) |
48 | 7, 39, 3, 13, 23, 15, 40, 41, 43, 44, 6, 45, 46, 47 | ply1remlem 26018 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) β (Monic1pβπ
) β§ (( deg1 βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) = 1 β§ (β‘((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) β { 0 }) = {π₯})) |
49 | 48 | simp1d 1141 |
. . . . . . 7
β’ ((π β§ π₯ β π) β ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) β (Monic1pβπ
)) |
50 | 38, 49 | elind 4194 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) β ((Baseβ(Poly1βπ)) β©
(Monic1pβπ
))) |
51 | | eqid 2731 |
. . . . . . . 8
β’
(Monic1pβπ) = (Monic1pβπ) |
52 | 7, 8, 9, 10, 2, 45, 51 | ressply1mon1p 33098 |
. . . . . . 7
β’ (π β
(Monic1pβπ) =
((Baseβ(Poly1βπ)) β© (Monic1pβπ
))) |
53 | 52 | adantr 480 |
. . . . . 6
β’ ((π β§ π₯ β π) β (Monic1pβπ) =
((Baseβ(Poly1βπ)) β© (Monic1pβπ
))) |
54 | 50, 53 | eleqtrrd 2835 |
. . . . 5
β’ ((π β§ π₯ β π) β ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) β (Monic1pβπ)) |
55 | | fveq2 6891 |
. . . . . . . 8
β’ (π = ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) β (πβπ) = (πβ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))) |
56 | 55 | fveq1d 6893 |
. . . . . . 7
β’ (π = ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) β ((πβπ)βπ₯) = ((πβ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))βπ₯)) |
57 | 56 | eqeq1d 2733 |
. . . . . 6
β’ (π = ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) β (((πβπ)βπ₯) = 0 β ((πβ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))βπ₯) = 0 )) |
58 | 57 | adantl 481 |
. . . . 5
β’ (((π β§ π₯ β π) β§ π = ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) β (((πβπ)βπ₯) = 0 β ((πβ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))βπ₯) = 0 )) |
59 | | irngval.o |
. . . . . . . . . 10
β’ π = (π
evalSub1 π) |
60 | 59, 3, 9, 8, 10, 41, 44, 11 | ressply1evl 33088 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π = ((eval1βπ
) βΎ
(Baseβ(Poly1βπ)))) |
61 | 60 | fveq1d 6893 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (πβ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) = (((eval1βπ
) βΎ (Baseβ(Poly1βπ)))β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))) |
62 | 38 | fvresd 6911 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (((eval1βπ
) βΎ
(Baseβ(Poly1βπ)))β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) = ((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))) |
63 | 61, 62 | eqtrd 2771 |
. . . . . . 7
β’ ((π β§ π₯ β π) β (πβ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) = ((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))) |
64 | 63 | fveq1d 6893 |
. . . . . 6
β’ ((π β§ π₯ β π) β ((πβ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))βπ₯) = (((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))βπ₯)) |
65 | | eqid 2731 |
. . . . . . . . 9
β’ (π
βs π΅) = (π
βs π΅) |
66 | | eqid 2731 |
. . . . . . . . 9
β’
(Baseβ(π
βs π΅)) = (Baseβ(π
βs π΅)) |
67 | 3 | fvexi 6905 |
. . . . . . . . . 10
β’ π΅ β V |
68 | 67 | a1i 11 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β π΅ β V) |
69 | 41, 7, 65, 3 | evl1rhm 22171 |
. . . . . . . . . . . 12
β’ (π
β CRing β
(eval1βπ
)
β ((Poly1βπ
) RingHom (π
βs π΅))) |
70 | 39, 66 | rhmf 20383 |
. . . . . . . . . . . 12
β’
((eval1βπ
) β ((Poly1βπ
) RingHom (π
βs π΅)) β (eval1βπ
):(Baseβ(Poly1βπ
))βΆ(Baseβ(π
βs π΅))) |
71 | 28, 69, 70 | 3syl 18 |
. . . . . . . . . . 11
β’ (π β
(eval1βπ
):(Baseβ(Poly1βπ
))βΆ(Baseβ(π
βs π΅))) |
72 | 71 | adantr 480 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β (eval1βπ
):(Baseβ(Poly1βπ
))βΆ(Baseβ(π
βs π΅))) |
73 | | eqid 2731 |
. . . . . . . . . . . . . 14
β’
(PwSer1βπ) = (PwSer1βπ) |
74 | | eqid 2731 |
. . . . . . . . . . . . . 14
β’
(Baseβ(PwSer1βπ)) =
(Baseβ(PwSer1βπ)) |
75 | 7, 8, 9, 10, 2, 73, 74, 39 | ressply1bas2 22070 |
. . . . . . . . . . . . 13
β’ (π β
(Baseβ(Poly1βπ)) =
((Baseβ(PwSer1βπ)) β©
(Baseβ(Poly1βπ
)))) |
76 | 75 | adantr 480 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β π) β
(Baseβ(Poly1βπ)) =
((Baseβ(PwSer1βπ)) β©
(Baseβ(Poly1βπ
)))) |
77 | 38, 76 | eleqtrd 2834 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β π) β ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) β
((Baseβ(PwSer1βπ)) β© (Baseβ(Poly1βπ
)))) |
78 | 77 | elin2d 4199 |
. . . . . . . . . 10
β’ ((π β§ π₯ β π) β ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)) β (Baseβ(Poly1βπ
))) |
79 | 72, 78 | ffvelcdmd 7087 |
. . . . . . . . 9
β’ ((π β§ π₯ β π) β ((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) β (Baseβ(π
βs π΅))) |
80 | 65, 3, 66, 43, 68, 79 | pwselbas 17442 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β ((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))):π΅βΆπ΅) |
81 | 80 | ffnd 6718 |
. . . . . . 7
β’ ((π β§ π₯ β π) β ((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) Fn π΅) |
82 | | vsnid 4665 |
. . . . . . . 8
β’ π₯ β {π₯} |
83 | 48 | simp3d 1143 |
. . . . . . . 8
β’ ((π β§ π₯ β π) β (β‘((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) β { 0 }) = {π₯}) |
84 | 82, 83 | eleqtrrid 2839 |
. . . . . . 7
β’ ((π β§ π₯ β π) β π₯ β (β‘((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) β { 0 })) |
85 | | fniniseg 7061 |
. . . . . . . 8
β’
(((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) Fn π΅ β (π₯ β (β‘((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) β { 0 }) β (π₯ β π΅ β§ (((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))βπ₯) = 0 ))) |
86 | 85 | simplbda 499 |
. . . . . . 7
β’
((((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) Fn π΅ β§ π₯ β (β‘((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯))) β { 0 })) β
(((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))βπ₯) = 0 ) |
87 | 81, 84, 86 | syl2anc 583 |
. . . . . 6
β’ ((π β§ π₯ β π) β (((eval1βπ
)β((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))βπ₯) = 0 ) |
88 | 64, 87 | eqtrd 2771 |
. . . . 5
β’ ((π β§ π₯ β π) β ((πβ((var1βπ
)(-gβ(Poly1βπ
))((algScβ(Poly1βπ
))βπ₯)))βπ₯) = 0 ) |
89 | 54, 58, 88 | rspcedvd 3614 |
. . . 4
β’ ((π β§ π₯ β π) β βπ β (Monic1pβπ)((πβπ)βπ₯) = 0 ) |
90 | 59, 8, 3, 47, 28, 2 | elirng 33206 |
. . . . 5
β’ (π β (π₯ β (π
IntgRing π) β (π₯ β π΅ β§ βπ β (Monic1pβπ)((πβπ)βπ₯) = 0 ))) |
91 | 90 | biimpar 477 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ βπ β (Monic1pβπ)((πβπ)βπ₯) = 0 )) β π₯ β (π
IntgRing π)) |
92 | 1, 6, 89, 91 | syl12anc 834 |
. . 3
β’ ((π β§ π₯ β π) β π₯ β (π
IntgRing π)) |
93 | 92 | ex 412 |
. 2
β’ (π β (π₯ β π β π₯ β (π
IntgRing π))) |
94 | 93 | ssrdv 3988 |
1
β’ (π β π β (π
IntgRing π)) |