Step | Hyp | Ref
| Expression |
1 | | hbtlem.s |
. . . . . 6
β’ π = (ldgIdlSeqβπ
) |
2 | | elex 3493 |
. . . . . . 7
β’ (π
β π β π
β V) |
3 | | fveq2 6892 |
. . . . . . . . . . . 12
β’ (π = π
β (Poly1βπ) =
(Poly1βπ
)) |
4 | | hbtlem.p |
. . . . . . . . . . . 12
β’ π = (Poly1βπ
) |
5 | 3, 4 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ (π = π
β (Poly1βπ) = π) |
6 | 5 | fveq2d 6896 |
. . . . . . . . . 10
β’ (π = π
β
(LIdealβ(Poly1βπ)) = (LIdealβπ)) |
7 | | hbtlem.u |
. . . . . . . . . 10
β’ π = (LIdealβπ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . . 9
β’ (π = π
β
(LIdealβ(Poly1βπ)) = π) |
9 | | fveq2 6892 |
. . . . . . . . . . . . . . . 16
β’ (π = π
β ( deg1 βπ) = ( deg1
βπ
)) |
10 | | hbtlem.d |
. . . . . . . . . . . . . . . 16
β’ π· = ( deg1
βπ
) |
11 | 9, 10 | eqtr4di 2791 |
. . . . . . . . . . . . . . 15
β’ (π = π
β ( deg1 βπ) = π·) |
12 | 11 | fveq1d 6894 |
. . . . . . . . . . . . . 14
β’ (π = π
β (( deg1 βπ)βπ) = (π·βπ)) |
13 | 12 | breq1d 5159 |
. . . . . . . . . . . . 13
β’ (π = π
β ((( deg1 βπ)βπ) β€ π₯ β (π·βπ) β€ π₯)) |
14 | 13 | anbi1d 631 |
. . . . . . . . . . . 12
β’ (π = π
β (((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯)) β ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯)))) |
15 | 14 | rexbidv 3179 |
. . . . . . . . . . 11
β’ (π = π
β (βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯)) β βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯)))) |
16 | 15 | abbidv 2802 |
. . . . . . . . . 10
β’ (π = π
β {π β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))} = {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}) |
17 | 16 | mpteq2dv 5251 |
. . . . . . . . 9
β’ (π = π
β (π₯ β β0 β¦ {π β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}) = (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))})) |
18 | 8, 17 | mpteq12dv 5240 |
. . . . . . . 8
β’ (π = π
β (π β
(LIdealβ(Poly1βπ)) β¦ (π₯ β β0 β¦ {π β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))})) = (π β π β¦ (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))) |
19 | | df-ldgis 41864 |
. . . . . . . 8
β’ ldgIdlSeq
= (π β V β¦
(π β
(LIdealβ(Poly1βπ)) β¦ (π₯ β β0 β¦ {π β£ βπ β π ((( deg1 βπ)βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))) |
20 | 18, 19, 7 | mptfvmpt 7230 |
. . . . . . 7
β’ (π
β V β
(ldgIdlSeqβπ
) =
(π β π β¦ (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))) |
21 | 2, 20 | syl 17 |
. . . . . 6
β’ (π
β π β (ldgIdlSeqβπ
) = (π β π β¦ (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))) |
22 | 1, 21 | eqtrid 2785 |
. . . . 5
β’ (π
β π β π = (π β π β¦ (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))) |
23 | 22 | fveq1d 6894 |
. . . 4
β’ (π
β π β (πβπΌ) = ((π β π β¦ (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))βπΌ)) |
24 | 23 | fveq1d 6894 |
. . 3
β’ (π
β π β ((πβπΌ)βπ) = (((π β π β¦ (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))βπΌ)βπ)) |
25 | 24 | 3ad2ant1 1134 |
. 2
β’ ((π
β π β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) = (((π β π β¦ (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))βπΌ)βπ)) |
26 | | rexeq 3322 |
. . . . . . 7
β’ (π = πΌ β (βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯)) β βπ β πΌ ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯)))) |
27 | 26 | abbidv 2802 |
. . . . . 6
β’ (π = πΌ β {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))} = {π β£ βπ β πΌ ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}) |
28 | 27 | mpteq2dv 5251 |
. . . . 5
β’ (π = πΌ β (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}) = (π₯ β β0 β¦ {π β£ βπ β πΌ ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))})) |
29 | | eqid 2733 |
. . . . 5
β’ (π β π β¦ (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))})) = (π β π β¦ (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))})) |
30 | | nn0ex 12478 |
. . . . . 6
β’
β0 β V |
31 | 30 | mptex 7225 |
. . . . 5
β’ (π₯ β β0
β¦ {π β£
βπ β πΌ ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}) β V |
32 | 28, 29, 31 | fvmpt 6999 |
. . . 4
β’ (πΌ β π β ((π β π β¦ (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))βπΌ) = (π₯ β β0 β¦ {π β£ βπ β πΌ ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))})) |
33 | 32 | fveq1d 6894 |
. . 3
β’ (πΌ β π β (((π β π β¦ (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))βπΌ)βπ) = ((π₯ β β0 β¦ {π β£ βπ β πΌ ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))})βπ)) |
34 | 33 | 3ad2ant2 1135 |
. 2
β’ ((π
β π β§ πΌ β π β§ π β β0) β (((π β π β¦ (π₯ β β0 β¦ {π β£ βπ β π ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}))βπΌ)βπ) = ((π₯ β β0 β¦ {π β£ βπ β πΌ ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))})βπ)) |
35 | | eqid 2733 |
. . 3
β’ (π₯ β β0
β¦ {π β£
βπ β πΌ ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}) = (π₯ β β0 β¦ {π β£ βπ β πΌ ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))}) |
36 | | breq2 5153 |
. . . . . 6
β’ (π₯ = π β ((π·βπ) β€ π₯ β (π·βπ) β€ π)) |
37 | | fveq2 6892 |
. . . . . . 7
β’ (π₯ = π β ((coe1βπ)βπ₯) = ((coe1βπ)βπ)) |
38 | 37 | eqeq2d 2744 |
. . . . . 6
β’ (π₯ = π β (π = ((coe1βπ)βπ₯) β π = ((coe1βπ)βπ))) |
39 | 36, 38 | anbi12d 632 |
. . . . 5
β’ (π₯ = π β (((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯)) β ((π·βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
40 | 39 | rexbidv 3179 |
. . . 4
β’ (π₯ = π β (βπ β πΌ ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯)) β βπ β πΌ ((π·βπ) β€ π β§ π = ((coe1βπ)βπ)))) |
41 | 40 | abbidv 2802 |
. . 3
β’ (π₯ = π β {π β£ βπ β πΌ ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))} = {π β£ βπ β πΌ ((π·βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
42 | | simp3 1139 |
. . 3
β’ ((π
β π β§ πΌ β π β§ π β β0) β π β
β0) |
43 | | simpr 486 |
. . . . . 6
β’ (((π·βπ) β€ π β§ π = ((coe1βπ)βπ)) β π = ((coe1βπ)βπ)) |
44 | 43 | reximi 3085 |
. . . . 5
β’
(βπ β
πΌ ((π·βπ) β€ π β§ π = ((coe1βπ)βπ)) β βπ β πΌ π = ((coe1βπ)βπ)) |
45 | 44 | ss2abi 4064 |
. . . 4
β’ {π β£ βπ β πΌ ((π·βπ) β€ π β§ π = ((coe1βπ)βπ))} β {π β£ βπ β πΌ π = ((coe1βπ)βπ)} |
46 | | abrexexg 7947 |
. . . . 5
β’ (πΌ β π β {π β£ βπ β πΌ π = ((coe1βπ)βπ)} β V) |
47 | 46 | 3ad2ant2 1135 |
. . . 4
β’ ((π
β π β§ πΌ β π β§ π β β0) β {π β£ βπ β πΌ π = ((coe1βπ)βπ)} β V) |
48 | | ssexg 5324 |
. . . 4
β’ (({π β£ βπ β πΌ ((π·βπ) β€ π β§ π = ((coe1βπ)βπ))} β {π β£ βπ β πΌ π = ((coe1βπ)βπ)} β§ {π β£ βπ β πΌ π = ((coe1βπ)βπ)} β V) β {π β£ βπ β πΌ ((π·βπ) β€ π β§ π = ((coe1βπ)βπ))} β V) |
49 | 45, 47, 48 | sylancr 588 |
. . 3
β’ ((π
β π β§ πΌ β π β§ π β β0) β {π β£ βπ β πΌ ((π·βπ) β€ π β§ π = ((coe1βπ)βπ))} β V) |
50 | 35, 41, 42, 49 | fvmptd3 7022 |
. 2
β’ ((π
β π β§ πΌ β π β§ π β β0) β ((π₯ β β0
β¦ {π β£
βπ β πΌ ((π·βπ) β€ π₯ β§ π = ((coe1βπ)βπ₯))})βπ) = {π β£ βπ β πΌ ((π·βπ) β€ π β§ π = ((coe1βπ)βπ))}) |
51 | 25, 34, 50 | 3eqtrd 2777 |
1
β’ ((π
β π β§ πΌ β π β§ π β β0) β ((πβπΌ)βπ) = {π β£ βπ β πΌ ((π·βπ) β€ π β§ π = ((coe1βπ)βπ))}) |