Step | Hyp | Ref
| Expression |
1 | | simpr 486 |
. . . . . . . . 9
β’ ((((
deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯)) β π¦ = ((coe1βπ)βπ₯)) |
2 | 1 | reximi 3088 |
. . . . . . . 8
β’
(βπ β
πΌ ((( deg1
βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯)) β βπ β πΌ π¦ = ((coe1βπ)βπ₯)) |
3 | 2 | ss2abi 4028 |
. . . . . . 7
β’ {π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))} β {π¦ β£ βπ β πΌ π¦ = ((coe1βπ)βπ₯)} |
4 | | abrexexg 7898 |
. . . . . . 7
β’ (πΌ β π β {π¦ β£ βπ β πΌ π¦ = ((coe1βπ)βπ₯)} β V) |
5 | | ssexg 5285 |
. . . . . . 7
β’ (({π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))} β {π¦ β£ βπ β πΌ π¦ = ((coe1βπ)βπ₯)} β§ {π¦ β£ βπ β πΌ π¦ = ((coe1βπ)βπ₯)} β V) β {π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))} β V) |
6 | 3, 4, 5 | sylancr 588 |
. . . . . 6
β’ (πΌ β π β {π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))} β V) |
7 | 6 | ralrimivw 3148 |
. . . . 5
β’ (πΌ β π β βπ₯ β β0 {π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))} β V) |
8 | 7 | adantl 483 |
. . . 4
β’ ((π
β Ring β§ πΌ β π) β βπ₯ β β0 {π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))} β V) |
9 | | eqid 2737 |
. . . . 5
β’ (π₯ β β0
β¦ {π¦ β£
βπ β πΌ ((( deg1
βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}) = (π₯ β β0 β¦ {π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}) |
10 | 9 | fnmpt 6646 |
. . . 4
β’
(βπ₯ β
β0 {π¦
β£ βπ β
πΌ ((( deg1
βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))} β V β (π₯ β β0 β¦ {π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}) Fn β0) |
11 | 8, 10 | syl 17 |
. . 3
β’ ((π
β Ring β§ πΌ β π) β (π₯ β β0 β¦ {π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}) Fn β0) |
12 | | hbtlem.s |
. . . . . . 7
β’ π = (ldgIdlSeqβπ
) |
13 | | elex 3466 |
. . . . . . . 8
β’ (π
β Ring β π
β V) |
14 | | fveq2 6847 |
. . . . . . . . . . . . 13
β’ (π = π
β (Poly1βπ) =
(Poly1βπ
)) |
15 | | hbtlem.p |
. . . . . . . . . . . . 13
β’ π = (Poly1βπ
) |
16 | 14, 15 | eqtr4di 2795 |
. . . . . . . . . . . 12
β’ (π = π
β (Poly1βπ) = π) |
17 | 16 | fveq2d 6851 |
. . . . . . . . . . 11
β’ (π = π
β
(LIdealβ(Poly1βπ)) = (LIdealβπ)) |
18 | | hbtlem.u |
. . . . . . . . . . 11
β’ π = (LIdealβπ) |
19 | 17, 18 | eqtr4di 2795 |
. . . . . . . . . 10
β’ (π = π
β
(LIdealβ(Poly1βπ)) = π) |
20 | | fveq2 6847 |
. . . . . . . . . . . . . . . 16
β’ (π = π
β ( deg1 βπ) = ( deg1
βπ
)) |
21 | 20 | fveq1d 6849 |
. . . . . . . . . . . . . . 15
β’ (π = π
β (( deg1 βπ)βπ) = (( deg1 βπ
)βπ)) |
22 | 21 | breq1d 5120 |
. . . . . . . . . . . . . 14
β’ (π = π
β ((( deg1 βπ)βπ) β€ π₯ β (( deg1 βπ
)βπ) β€ π₯)) |
23 | 22 | anbi1d 631 |
. . . . . . . . . . . . 13
β’ (π = π
β (((( deg1 βπ)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯)) β ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯)))) |
24 | 23 | rexbidv 3176 |
. . . . . . . . . . . 12
β’ (π = π
β (βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯)) β βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯)))) |
25 | 24 | abbidv 2806 |
. . . . . . . . . . 11
β’ (π = π
β {π¦ β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))} = {π¦ β£ βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}) |
26 | 25 | mpteq2dv 5212 |
. . . . . . . . . 10
β’ (π = π
β (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}) = (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))})) |
27 | 19, 26 | mpteq12dv 5201 |
. . . . . . . . 9
β’ (π = π
β (π β
(LIdealβ(Poly1βπ)) β¦ (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))})) = (π β π β¦ (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}))) |
28 | | df-ldgis 41478 |
. . . . . . . . 9
β’ ldgIdlSeq
= (π β V β¦
(π β
(LIdealβ(Poly1βπ)) β¦ (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}))) |
29 | 27, 28, 18 | mptfvmpt 7183 |
. . . . . . . 8
β’ (π
β V β
(ldgIdlSeqβπ
) =
(π β π β¦ (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}))) |
30 | 13, 29 | syl 17 |
. . . . . . 7
β’ (π
β Ring β
(ldgIdlSeqβπ
) =
(π β π β¦ (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}))) |
31 | 12, 30 | eqtrid 2789 |
. . . . . 6
β’ (π
β Ring β π = (π β π β¦ (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}))) |
32 | 31 | fveq1d 6849 |
. . . . 5
β’ (π
β Ring β (πβπΌ) = ((π β π β¦ (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}))βπΌ)) |
33 | | rexeq 3313 |
. . . . . . . 8
β’ (π = πΌ β (βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯)) β βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯)))) |
34 | 33 | abbidv 2806 |
. . . . . . 7
β’ (π = πΌ β {π¦ β£ βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))} = {π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}) |
35 | 34 | mpteq2dv 5212 |
. . . . . 6
β’ (π = πΌ β (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}) = (π₯ β β0 β¦ {π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))})) |
36 | | eqid 2737 |
. . . . . 6
β’ (π β π β¦ (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))})) = (π β π β¦ (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))})) |
37 | | nn0ex 12426 |
. . . . . . 7
β’
β0 β V |
38 | 37 | mptex 7178 |
. . . . . 6
β’ (π₯ β β0
β¦ {π¦ β£
βπ β πΌ ((( deg1
βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}) β V |
39 | 35, 36, 38 | fvmpt 6953 |
. . . . 5
β’ (πΌ β π β ((π β π β¦ (π₯ β β0 β¦ {π¦ β£ βπ β π ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}))βπΌ) = (π₯ β β0 β¦ {π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))})) |
40 | 32, 39 | sylan9eq 2797 |
. . . 4
β’ ((π
β Ring β§ πΌ β π) β (πβπΌ) = (π₯ β β0 β¦ {π¦ β£ βπ β πΌ ((( deg1 βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))})) |
41 | 40 | fneq1d 6600 |
. . 3
β’ ((π
β Ring β§ πΌ β π) β ((πβπΌ) Fn β0 β (π₯ β β0
β¦ {π¦ β£
βπ β πΌ ((( deg1
βπ
)βπ) β€ π₯ β§ π¦ = ((coe1βπ)βπ₯))}) Fn
β0)) |
42 | 11, 41 | mpbird 257 |
. 2
β’ ((π
β Ring β§ πΌ β π) β (πβπΌ) Fn β0) |
43 | | hbtlem7.t |
. . . . 5
β’ π = (LIdealβπ
) |
44 | 15, 18, 12, 43 | hbtlem2 41480 |
. . . 4
β’ ((π
β Ring β§ πΌ β π β§ π₯ β β0) β ((πβπΌ)βπ₯) β π) |
45 | 44 | 3expa 1119 |
. . 3
β’ (((π
β Ring β§ πΌ β π) β§ π₯ β β0) β ((πβπΌ)βπ₯) β π) |
46 | 45 | ralrimiva 3144 |
. 2
β’ ((π
β Ring β§ πΌ β π) β βπ₯ β β0 ((πβπΌ)βπ₯) β π) |
47 | | ffnfv 7071 |
. 2
β’ ((πβπΌ):β0βΆπ β ((πβπΌ) Fn β0 β§ βπ₯ β β0
((πβπΌ)βπ₯) β π)) |
48 | 42, 46, 47 | sylanbrc 584 |
1
β’ ((π
β Ring β§ πΌ β π) β (πβπΌ):β0βΆπ) |