Step | Hyp | Ref
| Expression |
1 | | hbtlem.p |
. . 3
β’ π = (Poly1βπ
) |
2 | | hbtlem.u |
. . 3
β’ π = (LIdealβπ) |
3 | | hbtlem.s |
. . 3
β’ π = (ldgIdlSeqβπ
) |
4 | | eqid 2732 |
. . 3
β’ (
deg1 βπ
) =
( deg1 βπ
) |
5 | 1, 2, 3, 4 | hbtlem1 41850 |
. 2
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
6 | | eqid 2732 |
. . . . . . . . . . . 12
β’
(Baseβπ) =
(Baseβπ) |
7 | 6, 2 | lidlss 20825 |
. . . . . . . . . . 11
β’ (πΌ β π β πΌ β (Baseβπ)) |
8 | 7 | 3ad2ant2 1134 |
. . . . . . . . . 10
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β πΌ β (Baseβπ)) |
9 | 8 | sselda 3981 |
. . . . . . . . 9
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ π β πΌ) β π β (Baseβπ)) |
10 | | eqid 2732 |
. . . . . . . . . 10
β’
(coe1βπ) = (coe1βπ) |
11 | | eqid 2732 |
. . . . . . . . . 10
β’
(Baseβπ
) =
(Baseβπ
) |
12 | 10, 6, 1, 11 | coe1f 21726 |
. . . . . . . . 9
β’ (π β (Baseβπ) β
(coe1βπ):β0βΆ(Baseβπ
)) |
13 | 9, 12 | syl 17 |
. . . . . . . 8
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ π β πΌ) β (coe1βπ):β0βΆ(Baseβπ
)) |
14 | | simpl3 1193 |
. . . . . . . 8
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ π β πΌ) β π β
β0) |
15 | 13, 14 | ffvelcdmd 7084 |
. . . . . . 7
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ π β πΌ) β ((coe1βπ)βπ) β (Baseβπ
)) |
16 | | eleq1a 2828 |
. . . . . . 7
β’
(((coe1βπ)βπ) β (Baseβπ
) β (π = ((coe1βπ)βπ) β π β (Baseβπ
))) |
17 | 15, 16 | syl 17 |
. . . . . 6
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ π β πΌ) β (π = ((coe1βπ)βπ) β π β (Baseβπ
))) |
18 | 17 | adantld 491 |
. . . . 5
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ π β πΌ) β (((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β π β (Baseβπ
))) |
19 | 18 | rexlimdva 3155 |
. . . 4
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β
(βπ β πΌ ((( deg1
βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β π β (Baseβπ
))) |
20 | 19 | abssdv 4064 |
. . 3
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β (Baseβπ
)) |
21 | 1 | ply1ring 21761 |
. . . . . . . 8
β’ (π
β Ring β π β Ring) |
22 | 21 | 3ad2ant1 1133 |
. . . . . . 7
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β π β Ring) |
23 | | simp2 1137 |
. . . . . . 7
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β πΌ β π) |
24 | | eqid 2732 |
. . . . . . . 8
β’
(0gβπ) = (0gβπ) |
25 | 2, 24 | lidl0cl 20827 |
. . . . . . 7
β’ ((π β Ring β§ πΌ β π) β (0gβπ) β πΌ) |
26 | 22, 23, 25 | syl2anc 584 |
. . . . . 6
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β
(0gβπ)
β πΌ) |
27 | 4, 1, 24 | deg1z 25596 |
. . . . . . . 8
β’ (π
β Ring β ((
deg1 βπ
)β(0gβπ)) = -β) |
28 | 27 | 3ad2ant1 1133 |
. . . . . . 7
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β ((
deg1 βπ
)β(0gβπ)) = -β) |
29 | | nn0ssre 12472 |
. . . . . . . . . 10
β’
β0 β β |
30 | | ressxr 11254 |
. . . . . . . . . 10
β’ β
β β* |
31 | 29, 30 | sstri 3990 |
. . . . . . . . 9
β’
β0 β β* |
32 | | simp3 1138 |
. . . . . . . . 9
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β π β
β0) |
33 | 31, 32 | sselid 3979 |
. . . . . . . 8
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β π β
β*) |
34 | | mnfle 13110 |
. . . . . . . 8
β’ (π β β*
β -β β€ π) |
35 | 33, 34 | syl 17 |
. . . . . . 7
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β -β
β€ π) |
36 | 28, 35 | eqbrtrd 5169 |
. . . . . 6
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β ((
deg1 βπ
)β(0gβπ)) β€ π) |
37 | | eqid 2732 |
. . . . . . . . . 10
β’
(0gβπ
) = (0gβπ
) |
38 | 1, 24, 37 | coe1z 21776 |
. . . . . . . . 9
β’ (π
β Ring β
(coe1β(0gβπ)) = (β0 Γ
{(0gβπ
)})) |
39 | 38 | 3ad2ant1 1133 |
. . . . . . . 8
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β
(coe1β(0gβπ)) = (β0 Γ
{(0gβπ
)})) |
40 | 39 | fveq1d 6890 |
. . . . . . 7
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β
((coe1β(0gβπ))βπ) = ((β0 Γ
{(0gβπ
)})βπ)) |
41 | | fvex 6901 |
. . . . . . . . 9
β’
(0gβπ
) β V |
42 | 41 | fvconst2 7201 |
. . . . . . . 8
β’ (π β β0
β ((β0 Γ {(0gβπ
)})βπ) = (0gβπ
)) |
43 | 42 | 3ad2ant3 1135 |
. . . . . . 7
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β
((β0 Γ {(0gβπ
)})βπ) = (0gβπ
)) |
44 | 40, 43 | eqtr2d 2773 |
. . . . . 6
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β
(0gβπ
) =
((coe1β(0gβπ))βπ)) |
45 | | fveq2 6888 |
. . . . . . . . 9
β’ (π = (0gβπ) β (( deg1
βπ
)βπ) = (( deg1
βπ
)β(0gβπ))) |
46 | 45 | breq1d 5157 |
. . . . . . . 8
β’ (π = (0gβπ) β ((( deg1
βπ
)βπ) β€ π β (( deg1 βπ
)β(0gβπ)) β€ π)) |
47 | | fveq2 6888 |
. . . . . . . . . 10
β’ (π = (0gβπ) β
(coe1βπ) =
(coe1β(0gβπ))) |
48 | 47 | fveq1d 6890 |
. . . . . . . . 9
β’ (π = (0gβπ) β
((coe1βπ)βπ) =
((coe1β(0gβπ))βπ)) |
49 | 48 | eqeq2d 2743 |
. . . . . . . 8
β’ (π = (0gβπ) β
((0gβπ
) =
((coe1βπ)βπ) β (0gβπ
) =
((coe1β(0gβπ))βπ))) |
50 | 46, 49 | anbi12d 631 |
. . . . . . 7
β’ (π = (0gβπ) β (((( deg1
βπ
)βπ) β€ π β§ (0gβπ
) =
((coe1βπ)βπ)) β ((( deg1 βπ
)β(0gβπ)) β€ π β§ (0gβπ
) =
((coe1β(0gβπ))βπ)))) |
51 | 50 | rspcev 3612 |
. . . . . 6
β’
(((0gβπ) β πΌ β§ ((( deg1 βπ
)β(0gβπ)) β€ π β§ (0gβπ
) =
((coe1β(0gβπ))βπ))) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ (0gβπ
) =
((coe1βπ)βπ))) |
52 | 26, 36, 44, 51 | syl12anc 835 |
. . . . 5
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β
βπ β πΌ ((( deg1
βπ
)βπ) β€ π β§ (0gβπ
) =
((coe1βπ)βπ))) |
53 | | eqeq1 2736 |
. . . . . . . 8
β’ (π = (0gβπ
) β (π = ((coe1βπ)βπ) β (0gβπ
) =
((coe1βπ)βπ))) |
54 | 53 | anbi2d 629 |
. . . . . . 7
β’ (π = (0gβπ
) β (((( deg1
βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β ((( deg1 βπ
)βπ) β€ π β§ (0gβπ
) =
((coe1βπ)βπ)))) |
55 | 54 | rexbidv 3178 |
. . . . . 6
β’ (π = (0gβπ
) β (βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ (0gβπ
) =
((coe1βπ)βπ)))) |
56 | 41, 55 | elab 3667 |
. . . . 5
β’
((0gβπ
) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ (0gβπ
) =
((coe1βπ)βπ))) |
57 | 52, 56 | sylibr 233 |
. . . 4
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β
(0gβπ
)
β {π β£
βπ β πΌ ((( deg1
βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
58 | 57 | ne0d 4334 |
. . 3
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β β
) |
59 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β π β Ring) |
60 | | simpl2 1192 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β πΌ β π) |
61 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’
(algScβπ) =
(algScβπ) |
62 | 1, 61, 11, 6 | ply1sclf 21798 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π
β Ring β
(algScβπ):(Baseβπ
)βΆ(Baseβπ)) |
63 | 62 | 3ad2ant1 1133 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β
(algScβπ):(Baseβπ
)βΆ(Baseβπ)) |
64 | 63 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β (algScβπ):(Baseβπ
)βΆ(Baseβπ)) |
65 | | simprl 769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β π β (Baseβπ
)) |
66 | 64, 65 | ffvelcdmd 7084 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β ((algScβπ)βπ) β (Baseβπ)) |
67 | | simprll 777 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π))) β π β πΌ) |
68 | 67 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β π β πΌ) |
69 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(.rβπ) = (.rβπ) |
70 | 2, 6, 69 | lidlmcl 20832 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β Ring β§ πΌ β π) β§ (((algScβπ)βπ) β (Baseβπ) β§ π β πΌ)) β (((algScβπ)βπ)(.rβπ)π) β πΌ) |
71 | 59, 60, 66, 68, 70 | syl22anc 837 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β (((algScβπ)βπ)(.rβπ)π) β πΌ) |
72 | | simprrl 779 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π))) β π β πΌ) |
73 | 72 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β π β πΌ) |
74 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’
(+gβπ) = (+gβπ) |
75 | 2, 74 | lidlacl 20828 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β Ring β§ πΌ β π) β§ ((((algScβπ)βπ)(.rβπ)π) β πΌ β§ π β πΌ)) β ((((algScβπ)βπ)(.rβπ)π)(+gβπ)π) β πΌ) |
76 | 59, 60, 71, 73, 75 | syl22anc 837 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β ((((algScβπ)βπ)(.rβπ)π)(+gβπ)π) β πΌ) |
77 | | simpl1 1191 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β π
β Ring) |
78 | 8 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β πΌ β (Baseβπ)) |
79 | 78, 68 | sseldd 3982 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β π β (Baseβπ)) |
80 | 6, 69 | ringcl 20066 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β Ring β§
((algScβπ)βπ) β (Baseβπ) β§ π β (Baseβπ)) β (((algScβπ)βπ)(.rβπ)π) β (Baseβπ)) |
81 | 59, 66, 79, 80 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β (((algScβπ)βπ)(.rβπ)π) β (Baseβπ)) |
82 | 78, 73 | sseldd 3982 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β π β (Baseβπ)) |
83 | | simpl3 1193 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β π β
β0) |
84 | 31, 83 | sselid 3979 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β π β
β*) |
85 | 4, 1, 6 | deg1xrcl 25591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
((((algScβπ)βπ)(.rβπ)π) β (Baseβπ) β (( deg1 βπ
)β(((algScβπ)βπ)(.rβπ)π)) β
β*) |
86 | 81, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β (( deg1 βπ
)β(((algScβπ)βπ)(.rβπ)π)) β
β*) |
87 | 4, 1, 6 | deg1xrcl 25591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π β (Baseβπ) β (( deg1
βπ
)βπ) β
β*) |
88 | 79, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β (( deg1 βπ
)βπ) β
β*) |
89 | 4, 1, 11, 6, 69, 61 | deg1mul3le 25625 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π
β Ring β§ π β (Baseβπ
) β§ π β (Baseβπ)) β (( deg1 βπ
)β(((algScβπ)βπ)(.rβπ)π)) β€ (( deg1 βπ
)βπ)) |
90 | 77, 65, 79, 89 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β (( deg1 βπ
)β(((algScβπ)βπ)(.rβπ)π)) β€ (( deg1 βπ
)βπ)) |
91 | | simprlr 778 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π))) β (( deg1 βπ
)βπ) β€ π) |
92 | 91 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β (( deg1 βπ
)βπ) β€ π) |
93 | 86, 88, 84, 90, 92 | xrletrd 13137 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β (( deg1 βπ
)β(((algScβπ)βπ)(.rβπ)π)) β€ π) |
94 | | simprrr 780 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π))) β (( deg1 βπ
)βπ) β€ π) |
95 | 94 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β (( deg1 βπ
)βπ) β€ π) |
96 | 1, 4, 77, 6, 74, 81, 82, 84, 93, 95 | deg1addle2 25611 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β (( deg1 βπ
)β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π)) β€ π) |
97 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’
(+gβπ
) = (+gβπ
) |
98 | 1, 6, 74, 97 | coe1addfv 21778 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β Ring β§
(((algScβπ)βπ)(.rβπ)π) β (Baseβπ) β§ π β (Baseβπ)) β§ π β β0) β
((coe1β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π))βπ) =
(((coe1β(((algScβπ)βπ)(.rβπ)π))βπ)(+gβπ
)((coe1βπ)βπ))) |
99 | 77, 81, 82, 83, 98 | syl31anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β
((coe1β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π))βπ) =
(((coe1β(((algScβπ)βπ)(.rβπ)π))βπ)(+gβπ
)((coe1βπ)βπ))) |
100 | | eqid 2732 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(.rβπ
) = (.rβπ
) |
101 | 1, 6, 11, 61, 69, 100 | coe1sclmulfv 21796 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((π
β Ring β§ (π β (Baseβπ
) β§ π β (Baseβπ)) β§ π β β0) β
((coe1β(((algScβπ)βπ)(.rβπ)π))βπ) = (π(.rβπ
)((coe1βπ)βπ))) |
102 | 77, 65, 79, 83, 101 | syl121anc 1375 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β
((coe1β(((algScβπ)βπ)(.rβπ)π))βπ) = (π(.rβπ
)((coe1βπ)βπ))) |
103 | 102 | oveq1d 7420 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β
(((coe1β(((algScβπ)βπ)(.rβπ)π))βπ)(+gβπ
)((coe1βπ)βπ)) = ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ))) |
104 | 99, 103 | eqtr2d 2773 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) =
((coe1β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π))βπ)) |
105 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = ((((algScβπ)βπ)(.rβπ)π)(+gβπ)π) β (( deg1 βπ
)βπ) = (( deg1 βπ
)β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π))) |
106 | 105 | breq1d 5157 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = ((((algScβπ)βπ)(.rβπ)π)(+gβπ)π) β ((( deg1 βπ
)βπ) β€ π β (( deg1 βπ
)β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π)) β€ π)) |
107 | | fveq2 6888 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π = ((((algScβπ)βπ)(.rβπ)π)(+gβπ)π) β (coe1βπ) =
(coe1β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π))) |
108 | 107 | fveq1d 6890 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (π = ((((algScβπ)βπ)(.rβπ)π)(+gβπ)π) β ((coe1βπ)βπ) =
((coe1β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π))βπ)) |
109 | 108 | eqeq2d 2743 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = ((((algScβπ)βπ)(.rβπ)π)(+gβπ)π) β (((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) = ((coe1βπ)βπ) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) =
((coe1β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π))βπ))) |
110 | 106, 109 | anbi12d 631 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = ((((algScβπ)βπ)(.rβπ)π)(+gβπ)π) β (((( deg1 βπ
)βπ) β€ π β§ ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) = ((coe1βπ)βπ)) β ((( deg1 βπ
)β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π)) β€ π β§ ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) =
((coe1β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π))βπ)))) |
111 | 110 | rspcev 3612 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((((((algScβπ)βπ)(.rβπ)π)(+gβπ)π) β πΌ β§ ((( deg1 βπ
)β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π)) β€ π β§ ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) =
((coe1β((((algScβπ)βπ)(.rβπ)π)(+gβπ)π))βπ))) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) = ((coe1βπ)βπ))) |
112 | 76, 96, 104, 111 | syl12anc 835 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) = ((coe1βπ)βπ))) |
113 | | ovex 7438 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) β V |
114 | | eqeq1 2736 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π = ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) β (π = ((coe1βπ)βπ) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) = ((coe1βπ)βπ))) |
115 | 114 | anbi2d 629 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) β (((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β ((( deg1 βπ
)βπ) β€ π β§ ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) = ((coe1βπ)βπ)))) |
116 | 115 | rexbidv 3178 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) β (βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) = ((coe1βπ)βπ)))) |
117 | 113, 116 | elab 3667 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) = ((coe1βπ)βπ))) |
118 | 112, 117 | sylibr 233 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ (π β (Baseβπ
) β§ ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β§ (π β πΌ β§ (( deg1 βπ
)βπ) β€ π)))) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
119 | 118 | exp45 439 |
. . . . . . . . . . . . . . . . . 18
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β (π β (Baseβπ
) β ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})))) |
120 | 119 | imp 407 |
. . . . . . . . . . . . . . . . 17
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β ((π β πΌ β§ (( deg1 βπ
)βπ) β€ π) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}))) |
121 | 120 | exp5c 445 |
. . . . . . . . . . . . . . . 16
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β (π β πΌ β ((( deg1 βπ
)βπ) β€ π β (π β πΌ β ((( deg1 βπ
)βπ) β€ π β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}))))) |
122 | 121 | imp 407 |
. . . . . . . . . . . . . . 15
β’ ((((π
β Ring β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β§ π β πΌ) β ((( deg1 βπ
)βπ) β€ π β (π β πΌ β ((( deg1 βπ
)βπ) β€ π β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})))) |
123 | 122 | imp41 426 |
. . . . . . . . . . . . . 14
β’
(((((((π
β Ring
β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
124 | | oveq2 7413 |
. . . . . . . . . . . . . . 15
β’ (π = ((coe1βπ)βπ) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)π) = ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ))) |
125 | 124 | eleq1d 2818 |
. . . . . . . . . . . . . 14
β’ (π = ((coe1βπ)βπ) β (((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)((coe1βπ)βπ)) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
126 | 123, 125 | syl5ibrcom 246 |
. . . . . . . . . . . . 13
β’
(((((((π
β Ring
β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β (π = ((coe1βπ)βπ) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
127 | 126 | expimpd 454 |
. . . . . . . . . . . 12
β’
((((((π
β Ring
β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β§ π β πΌ) β (((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
128 | 127 | rexlimdva 3155 |
. . . . . . . . . . 11
β’
(((((π
β Ring
β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β (βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
129 | 128 | alrimiv 1930 |
. . . . . . . . . 10
β’
(((((π
β Ring
β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β βπ(βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
130 | | eqeq1 2736 |
. . . . . . . . . . . . . 14
β’ (π = π β (π = ((coe1βπ)βπ) β π = ((coe1βπ)βπ))) |
131 | 130 | anbi2d 629 |
. . . . . . . . . . . . 13
β’ (π = π β (((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
132 | 131 | rexbidv 3178 |
. . . . . . . . . . . 12
β’ (π = π β (βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
133 | | fveq2 6888 |
. . . . . . . . . . . . . . 15
β’ (π = π β (( deg1 βπ
)βπ) = (( deg1 βπ
)βπ)) |
134 | 133 | breq1d 5157 |
. . . . . . . . . . . . . 14
β’ (π = π β ((( deg1 βπ
)βπ) β€ π β (( deg1 βπ
)βπ) β€ π)) |
135 | | fveq2 6888 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (coe1βπ) = (coe1βπ)) |
136 | 135 | fveq1d 6890 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((coe1βπ)βπ) = ((coe1βπ)βπ)) |
137 | 136 | eqeq2d 2743 |
. . . . . . . . . . . . . 14
β’ (π = π β (π = ((coe1βπ)βπ) β π = ((coe1βπ)βπ))) |
138 | 134, 137 | anbi12d 631 |
. . . . . . . . . . . . 13
β’ (π = π β (((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
139 | 138 | cbvrexvw 3235 |
. . . . . . . . . . . 12
β’
(βπ β
πΌ ((( deg1
βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))) |
140 | 132, 139 | bitrdi 286 |
. . . . . . . . . . 11
β’ (π = π β (βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
141 | 140 | ralab 3686 |
. . . . . . . . . 10
β’
(βπ β
{π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β βπ(βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
142 | 129, 141 | sylibr 233 |
. . . . . . . . 9
β’
(((((π
β Ring
β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
143 | | oveq2 7413 |
. . . . . . . . . . . 12
β’ (π = ((coe1βπ)βπ) β (π(.rβπ
)π) = (π(.rβπ
)((coe1βπ)βπ))) |
144 | 143 | oveq1d 7420 |
. . . . . . . . . . 11
β’ (π = ((coe1βπ)βπ) β ((π(.rβπ
)π)(+gβπ
)π) = ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)π)) |
145 | 144 | eleq1d 2818 |
. . . . . . . . . 10
β’ (π = ((coe1βπ)βπ) β (((π(.rβπ
)π)(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
146 | 145 | ralbidv 3177 |
. . . . . . . . 9
β’ (π = ((coe1βπ)βπ) β (βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)π)(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)((coe1βπ)βπ))(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
147 | 142, 146 | syl5ibrcom 246 |
. . . . . . . 8
β’
(((((π
β Ring
β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β§ π β πΌ) β§ (( deg1 βπ
)βπ) β€ π) β (π = ((coe1βπ)βπ) β βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)π)(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
148 | 147 | expimpd 454 |
. . . . . . 7
β’ ((((π
β Ring β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β§ π β πΌ) β (((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)π)(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
149 | 148 | rexlimdva 3155 |
. . . . . 6
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β (βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)π)(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
150 | 149 | alrimiv 1930 |
. . . . 5
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β βπ(βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)π)(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
151 | | eqeq1 2736 |
. . . . . . . . 9
β’ (π = π β (π = ((coe1βπ)βπ) β π = ((coe1βπ)βπ))) |
152 | 151 | anbi2d 629 |
. . . . . . . 8
β’ (π = π β (((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
153 | 152 | rexbidv 3178 |
. . . . . . 7
β’ (π = π β (βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
154 | | fveq2 6888 |
. . . . . . . . . 10
β’ (π = π β (( deg1 βπ
)βπ) = (( deg1 βπ
)βπ)) |
155 | 154 | breq1d 5157 |
. . . . . . . . 9
β’ (π = π β ((( deg1 βπ
)βπ) β€ π β (( deg1 βπ
)βπ) β€ π)) |
156 | | fveq2 6888 |
. . . . . . . . . . 11
β’ (π = π β (coe1βπ) = (coe1βπ)) |
157 | 156 | fveq1d 6890 |
. . . . . . . . . 10
β’ (π = π β ((coe1βπ)βπ) = ((coe1βπ)βπ)) |
158 | 157 | eqeq2d 2743 |
. . . . . . . . 9
β’ (π = π β (π = ((coe1βπ)βπ) β π = ((coe1βπ)βπ))) |
159 | 155, 158 | anbi12d 631 |
. . . . . . . 8
β’ (π = π β (((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
160 | 159 | cbvrexvw 3235 |
. . . . . . 7
β’
(βπ β
πΌ ((( deg1
βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))) |
161 | 153, 160 | bitrdi 286 |
. . . . . 6
β’ (π = π β (βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
162 | 161 | ralab 3686 |
. . . . 5
β’
(βπ β
{π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)π)(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β βπ(βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)π)(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
163 | 150, 162 | sylibr 233 |
. . . 4
β’ (((π
β Ring β§ πΌ β π β§ π β β0) β§ π β (Baseβπ
)) β βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)π)(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
164 | 163 | ralrimiva 3146 |
. . 3
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β
βπ β
(Baseβπ
)βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)π)(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
165 | | hbtlem2.t |
. . . 4
β’ π = (LIdealβπ
) |
166 | 165, 11, 97, 100 | islidl 20826 |
. . 3
β’ ({π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β π β ({π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β (Baseβπ
) β§ {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β β
β§ βπ β (Baseβπ
)βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))}βπ β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} ((π(.rβπ
)π)(+gβπ
)π) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))})) |
167 | 20, 58, 164, 166 | syl3anbrc 1343 |
. 2
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β {π β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π β§ π = ((coe1βπ)βπ))} β π) |
168 | 5, 167 | eqeltrd 2833 |
1
β’ ((π
β Ring β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) β π) |