Step | Hyp | Ref
| Expression |
1 | | fta1.3 |
. . . . . . . . . 10
β’ (π β πΉ β ((Polyββ) β
{0π})) |
2 | | eldifsn 4791 |
. . . . . . . . . 10
β’ (πΉ β ((Polyββ)
β {0π}) β (πΉ β (Polyββ) β§ πΉ β
0π)) |
3 | 1, 2 | sylib 217 |
. . . . . . . . 9
β’ (π β (πΉ β (Polyββ) β§ πΉ β
0π)) |
4 | 3 | simpld 496 |
. . . . . . . 8
β’ (π β πΉ β
(Polyββ)) |
5 | | fta1.5 |
. . . . . . . . . 10
β’ (π β π΄ β (β‘πΉ β {0})) |
6 | | plyf 25712 |
. . . . . . . . . . 11
β’ (πΉ β (Polyββ)
β πΉ:ββΆβ) |
7 | | ffn 6718 |
. . . . . . . . . . 11
β’ (πΉ:ββΆβ β
πΉ Fn
β) |
8 | | fniniseg 7062 |
. . . . . . . . . . 11
β’ (πΉ Fn β β (π΄ β (β‘πΉ β {0}) β (π΄ β β β§ (πΉβπ΄) = 0))) |
9 | 4, 6, 7, 8 | 4syl 19 |
. . . . . . . . . 10
β’ (π β (π΄ β (β‘πΉ β {0}) β (π΄ β β β§ (πΉβπ΄) = 0))) |
10 | 5, 9 | mpbid 231 |
. . . . . . . . 9
β’ (π β (π΄ β β β§ (πΉβπ΄) = 0)) |
11 | 10 | simpld 496 |
. . . . . . . 8
β’ (π β π΄ β β) |
12 | 10 | simprd 497 |
. . . . . . . 8
β’ (π β (πΉβπ΄) = 0) |
13 | | eqid 2733 |
. . . . . . . . 9
β’
(Xp βf β (β Γ
{π΄})) =
(Xp βf β (β Γ {π΄})) |
14 | 13 | facth 25819 |
. . . . . . . 8
β’ ((πΉ β (Polyββ)
β§ π΄ β β
β§ (πΉβπ΄) = 0) β πΉ = ((Xp
βf β (β Γ {π΄})) βf Β· (πΉ quot (Xp
βf β (β Γ {π΄}))))) |
15 | 4, 11, 12, 14 | syl3anc 1372 |
. . . . . . 7
β’ (π β πΉ = ((Xp
βf β (β Γ {π΄})) βf Β· (πΉ quot (Xp
βf β (β Γ {π΄}))))) |
16 | 15 | cnveqd 5876 |
. . . . . 6
β’ (π β β‘πΉ = β‘((Xp βf
β (β Γ {π΄})) βf Β· (πΉ quot (Xp
βf β (β Γ {π΄}))))) |
17 | 16 | imaeq1d 6059 |
. . . . 5
β’ (π β (β‘πΉ β {0}) = (β‘((Xp βf
β (β Γ {π΄})) βf Β· (πΉ quot (Xp
βf β (β Γ {π΄})))) β {0})) |
18 | | cnex 11191 |
. . . . . . 7
β’ β
β V |
19 | 18 | a1i 11 |
. . . . . 6
β’ (π β β β
V) |
20 | | ssid 4005 |
. . . . . . . . 9
β’ β
β β |
21 | | ax-1cn 11168 |
. . . . . . . . 9
β’ 1 β
β |
22 | | plyid 25723 |
. . . . . . . . 9
β’ ((β
β β β§ 1 β β) β Xp β
(Polyββ)) |
23 | 20, 21, 22 | mp2an 691 |
. . . . . . . 8
β’
Xp β (Polyββ) |
24 | | plyconst 25720 |
. . . . . . . . 9
β’ ((β
β β β§ π΄
β β) β (β Γ {π΄}) β
(Polyββ)) |
25 | 20, 11, 24 | sylancr 588 |
. . . . . . . 8
β’ (π β (β Γ {π΄}) β
(Polyββ)) |
26 | | plysubcl 25736 |
. . . . . . . 8
β’
((Xp β (Polyββ) β§ (β
Γ {π΄}) β
(Polyββ)) β (Xp βf β
(β Γ {π΄}))
β (Polyββ)) |
27 | 23, 25, 26 | sylancr 588 |
. . . . . . 7
β’ (π β (Xp
βf β (β Γ {π΄})) β
(Polyββ)) |
28 | | plyf 25712 |
. . . . . . 7
β’
((Xp βf β (β Γ
{π΄})) β
(Polyββ) β (Xp βf β
(β Γ {π΄})):ββΆβ) |
29 | 27, 28 | syl 17 |
. . . . . 6
β’ (π β (Xp
βf β (β Γ {π΄})):ββΆβ) |
30 | 13 | plyremlem 25817 |
. . . . . . . . . . . 12
β’ (π΄ β β β
((Xp βf β (β Γ {π΄})) β (Polyββ)
β§ (degβ(Xp βf β (β
Γ {π΄}))) = 1 β§
(β‘(Xp
βf β (β Γ {π΄})) β {0}) = {π΄})) |
31 | 11, 30 | syl 17 |
. . . . . . . . . . 11
β’ (π β ((Xp
βf β (β Γ {π΄})) β (Polyββ) β§
(degβ(Xp βf β (β Γ
{π΄}))) = 1 β§ (β‘(Xp βf
β (β Γ {π΄})) β {0}) = {π΄})) |
32 | 31 | simp2d 1144 |
. . . . . . . . . 10
β’ (π β
(degβ(Xp βf β (β Γ
{π΄}))) =
1) |
33 | | ax-1ne0 11179 |
. . . . . . . . . . 11
β’ 1 β
0 |
34 | 33 | a1i 11 |
. . . . . . . . . 10
β’ (π β 1 β 0) |
35 | 32, 34 | eqnetrd 3009 |
. . . . . . . . 9
β’ (π β
(degβ(Xp βf β (β Γ
{π΄}))) β
0) |
36 | | fveq2 6892 |
. . . . . . . . . . 11
β’
((Xp βf β (β Γ
{π΄})) =
0π β (degβ(Xp
βf β (β Γ {π΄}))) =
(degβ0π)) |
37 | | dgr0 25776 |
. . . . . . . . . . 11
β’
(degβ0π) = 0 |
38 | 36, 37 | eqtrdi 2789 |
. . . . . . . . . 10
β’
((Xp βf β (β Γ
{π΄})) =
0π β (degβ(Xp
βf β (β Γ {π΄}))) = 0) |
39 | 38 | necon3i 2974 |
. . . . . . . . 9
β’
((degβ(Xp βf β (β
Γ {π΄}))) β 0
β (Xp βf β (β Γ
{π΄})) β
0π) |
40 | 35, 39 | syl 17 |
. . . . . . . 8
β’ (π β (Xp
βf β (β Γ {π΄})) β
0π) |
41 | | quotcl2 25815 |
. . . . . . . 8
β’ ((πΉ β (Polyββ)
β§ (Xp βf β (β Γ {π΄})) β (Polyββ)
β§ (Xp βf β (β Γ {π΄})) β 0π)
β (πΉ quot
(Xp βf β (β Γ {π΄}))) β
(Polyββ)) |
42 | 4, 27, 40, 41 | syl3anc 1372 |
. . . . . . 7
β’ (π β (πΉ quot (Xp
βf β (β Γ {π΄}))) β
(Polyββ)) |
43 | | plyf 25712 |
. . . . . . 7
β’ ((πΉ quot (Xp
βf β (β Γ {π΄}))) β (Polyββ) β
(πΉ quot
(Xp βf β (β Γ {π΄}))):ββΆβ) |
44 | 42, 43 | syl 17 |
. . . . . 6
β’ (π β (πΉ quot (Xp
βf β (β Γ {π΄}))):ββΆβ) |
45 | | ofmulrt 25795 |
. . . . . 6
β’ ((β
β V β§ (Xp βf β (β
Γ {π΄})):ββΆβ β§ (πΉ quot (Xp
βf β (β Γ {π΄}))):ββΆβ) β (β‘((Xp βf
β (β Γ {π΄})) βf Β· (πΉ quot (Xp
βf β (β Γ {π΄})))) β {0}) = ((β‘(Xp βf
β (β Γ {π΄})) β {0}) βͺ (β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}))) |
46 | 19, 29, 44, 45 | syl3anc 1372 |
. . . . 5
β’ (π β (β‘((Xp βf
β (β Γ {π΄})) βf Β· (πΉ quot (Xp
βf β (β Γ {π΄})))) β {0}) = ((β‘(Xp βf
β (β Γ {π΄})) β {0}) βͺ (β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}))) |
47 | 31 | simp3d 1145 |
. . . . . 6
β’ (π β (β‘(Xp βf
β (β Γ {π΄})) β {0}) = {π΄}) |
48 | 47 | uneq1d 4163 |
. . . . 5
β’ (π β ((β‘(Xp βf
β (β Γ {π΄})) β {0}) βͺ (β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) = ({π΄} βͺ (β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}))) |
49 | 17, 46, 48 | 3eqtrd 2777 |
. . . 4
β’ (π β (β‘πΉ β {0}) = ({π΄} βͺ (β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}))) |
50 | | fta1.1 |
. . . 4
β’ π
= (β‘πΉ β {0}) |
51 | | uncom 4154 |
. . . 4
β’ ((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄}) = ({π΄} βͺ (β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) |
52 | 49, 50, 51 | 3eqtr4g 2798 |
. . 3
β’ (π β π
= ((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄})) |
53 | 21 | a1i 11 |
. . . . . . 7
β’ (π β 1 β
β) |
54 | | dgrcl 25747 |
. . . . . . . . 9
β’ ((πΉ quot (Xp
βf β (β Γ {π΄}))) β (Polyββ) β
(degβ(πΉ quot
(Xp βf β (β Γ {π΄})))) β
β0) |
55 | 42, 54 | syl 17 |
. . . . . . . 8
β’ (π β (degβ(πΉ quot (Xp
βf β (β Γ {π΄})))) β
β0) |
56 | 55 | nn0cnd 12534 |
. . . . . . 7
β’ (π β (degβ(πΉ quot (Xp
βf β (β Γ {π΄})))) β β) |
57 | | fta1.2 |
. . . . . . . 8
β’ (π β π· β
β0) |
58 | 57 | nn0cnd 12534 |
. . . . . . 7
β’ (π β π· β β) |
59 | | addcom 11400 |
. . . . . . . . 9
β’ ((1
β β β§ π·
β β) β (1 + π·) = (π· + 1)) |
60 | 21, 58, 59 | sylancr 588 |
. . . . . . . 8
β’ (π β (1 + π·) = (π· + 1)) |
61 | 15 | fveq2d 6896 |
. . . . . . . . 9
β’ (π β (degβπΉ) =
(degβ((Xp βf β (β Γ
{π΄})) βf
Β· (πΉ quot
(Xp βf β (β Γ {π΄})))))) |
62 | | fta1.4 |
. . . . . . . . 9
β’ (π β (degβπΉ) = (π· + 1)) |
63 | 3 | simprd 497 |
. . . . . . . . . . . 12
β’ (π β πΉ β
0π) |
64 | 15 | eqcomd 2739 |
. . . . . . . . . . . 12
β’ (π β ((Xp
βf β (β Γ {π΄})) βf Β· (πΉ quot (Xp
βf β (β Γ {π΄})))) = πΉ) |
65 | | 0cnd 11207 |
. . . . . . . . . . . . . 14
β’ (π β 0 β
β) |
66 | | mul01 11393 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β (π₯ Β· 0) =
0) |
67 | 66 | adantl 483 |
. . . . . . . . . . . . . 14
β’ ((π β§ π₯ β β) β (π₯ Β· 0) = 0) |
68 | 19, 29, 65, 65, 67 | caofid1 7703 |
. . . . . . . . . . . . 13
β’ (π β ((Xp
βf β (β Γ {π΄})) βf Β· (β
Γ {0})) = (β Γ {0})) |
69 | | df-0p 25187 |
. . . . . . . . . . . . . 14
β’
0π = (β Γ {0}) |
70 | 69 | oveq2i 7420 |
. . . . . . . . . . . . 13
β’
((Xp βf β (β Γ
{π΄})) βf
Β· 0π) = ((Xp βf
β (β Γ {π΄})) βf Β· (β
Γ {0})) |
71 | 68, 70, 69 | 3eqtr4g 2798 |
. . . . . . . . . . . 12
β’ (π β ((Xp
βf β (β Γ {π΄})) βf Β·
0π) = 0π) |
72 | 63, 64, 71 | 3netr4d 3019 |
. . . . . . . . . . 11
β’ (π β ((Xp
βf β (β Γ {π΄})) βf Β· (πΉ quot (Xp
βf β (β Γ {π΄})))) β ((Xp
βf β (β Γ {π΄})) βf Β·
0π)) |
73 | | oveq2 7417 |
. . . . . . . . . . . 12
β’ ((πΉ quot (Xp
βf β (β Γ {π΄}))) = 0π β
((Xp βf β (β Γ {π΄})) βf Β·
(πΉ quot
(Xp βf β (β Γ {π΄})))) = ((Xp
βf β (β Γ {π΄})) βf Β·
0π)) |
74 | 73 | necon3i 2974 |
. . . . . . . . . . 11
β’
(((Xp βf β (β Γ
{π΄})) βf
Β· (πΉ quot
(Xp βf β (β Γ {π΄})))) β
((Xp βf β (β Γ {π΄})) βf Β·
0π) β (πΉ quot (Xp
βf β (β Γ {π΄}))) β
0π) |
75 | 72, 74 | syl 17 |
. . . . . . . . . 10
β’ (π β (πΉ quot (Xp
βf β (β Γ {π΄}))) β
0π) |
76 | | eqid 2733 |
. . . . . . . . . . 11
β’
(degβ(Xp βf β (β
Γ {π΄}))) =
(degβ(Xp βf β (β Γ
{π΄}))) |
77 | | eqid 2733 |
. . . . . . . . . . 11
β’
(degβ(πΉ quot
(Xp βf β (β Γ {π΄})))) = (degβ(πΉ quot (Xp
βf β (β Γ {π΄})))) |
78 | 76, 77 | dgrmul 25784 |
. . . . . . . . . 10
β’
((((Xp βf β (β Γ
{π΄})) β
(Polyββ) β§ (Xp βf β
(β Γ {π΄})) β
0π) β§ ((πΉ quot (Xp
βf β (β Γ {π΄}))) β (Polyββ) β§
(πΉ quot
(Xp βf β (β Γ {π΄}))) β
0π)) β (degβ((Xp
βf β (β Γ {π΄})) βf Β· (πΉ quot (Xp
βf β (β Γ {π΄}))))) = ((degβ(Xp
βf β (β Γ {π΄}))) + (degβ(πΉ quot (Xp
βf β (β Γ {π΄})))))) |
79 | 27, 40, 42, 75, 78 | syl22anc 838 |
. . . . . . . . 9
β’ (π β
(degβ((Xp βf β (β Γ
{π΄})) βf
Β· (πΉ quot
(Xp βf β (β Γ {π΄}))))) =
((degβ(Xp βf β (β Γ
{π΄}))) + (degβ(πΉ quot (Xp
βf β (β Γ {π΄})))))) |
80 | 61, 62, 79 | 3eqtr3d 2781 |
. . . . . . . 8
β’ (π β (π· + 1) = ((degβ(Xp
βf β (β Γ {π΄}))) + (degβ(πΉ quot (Xp
βf β (β Γ {π΄})))))) |
81 | 32 | oveq1d 7424 |
. . . . . . . 8
β’ (π β
((degβ(Xp βf β (β Γ
{π΄}))) + (degβ(πΉ quot (Xp
βf β (β Γ {π΄}))))) = (1 + (degβ(πΉ quot (Xp
βf β (β Γ {π΄})))))) |
82 | 60, 80, 81 | 3eqtrrd 2778 |
. . . . . . 7
β’ (π β (1 + (degβ(πΉ quot (Xp
βf β (β Γ {π΄}))))) = (1 + π·)) |
83 | 53, 56, 58, 82 | addcanad 11419 |
. . . . . 6
β’ (π β (degβ(πΉ quot (Xp
βf β (β Γ {π΄})))) = π·) |
84 | | fveqeq2 6901 |
. . . . . . . 8
β’ (π = (πΉ quot (Xp
βf β (β Γ {π΄}))) β ((degβπ) = π· β (degβ(πΉ quot (Xp
βf β (β Γ {π΄})))) = π·)) |
85 | | cnveq 5874 |
. . . . . . . . . . 11
β’ (π = (πΉ quot (Xp
βf β (β Γ {π΄}))) β β‘π = β‘(πΉ quot (Xp
βf β (β Γ {π΄})))) |
86 | 85 | imaeq1d 6059 |
. . . . . . . . . 10
β’ (π = (πΉ quot (Xp
βf β (β Γ {π΄}))) β (β‘π β {0}) = (β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) |
87 | 86 | eleq1d 2819 |
. . . . . . . . 9
β’ (π = (πΉ quot (Xp
βf β (β Γ {π΄}))) β ((β‘π β {0}) β Fin β (β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) β
Fin)) |
88 | 86 | fveq2d 6896 |
. . . . . . . . . 10
β’ (π = (πΉ quot (Xp
βf β (β Γ {π΄}))) β (β―β(β‘π β {0})) = (β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}))) |
89 | | fveq2 6892 |
. . . . . . . . . 10
β’ (π = (πΉ quot (Xp
βf β (β Γ {π΄}))) β (degβπ) = (degβ(πΉ quot (Xp
βf β (β Γ {π΄}))))) |
90 | 88, 89 | breq12d 5162 |
. . . . . . . . 9
β’ (π = (πΉ quot (Xp
βf β (β Γ {π΄}))) β ((β―β(β‘π β {0})) β€ (degβπ) β (β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) β€ (degβ(πΉ quot (Xp
βf β (β Γ {π΄})))))) |
91 | 87, 90 | anbi12d 632 |
. . . . . . . 8
β’ (π = (πΉ quot (Xp
βf β (β Γ {π΄}))) β (((β‘π β {0}) β Fin β§
(β―β(β‘π β {0})) β€ (degβπ)) β ((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) β Fin β§
(β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) β€ (degβ(πΉ quot (Xp
βf β (β Γ {π΄}))))))) |
92 | 84, 91 | imbi12d 345 |
. . . . . . 7
β’ (π = (πΉ quot (Xp
βf β (β Γ {π΄}))) β (((degβπ) = π· β ((β‘π β {0}) β Fin β§
(β―β(β‘π β {0})) β€ (degβπ))) β ((degβ(πΉ quot (Xp
βf β (β Γ {π΄})))) = π· β ((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) β Fin β§
(β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) β€ (degβ(πΉ quot (Xp
βf β (β Γ {π΄})))))))) |
93 | | fta1.6 |
. . . . . . 7
β’ (π β βπ β ((Polyββ) β
{0π})((degβπ) = π· β ((β‘π β {0}) β Fin β§
(β―β(β‘π β {0})) β€ (degβπ)))) |
94 | | eldifsn 4791 |
. . . . . . . 8
β’ ((πΉ quot (Xp
βf β (β Γ {π΄}))) β ((Polyββ) β
{0π}) β ((πΉ quot (Xp
βf β (β Γ {π΄}))) β (Polyββ) β§
(πΉ quot
(Xp βf β (β Γ {π΄}))) β
0π)) |
95 | 42, 75, 94 | sylanbrc 584 |
. . . . . . 7
β’ (π β (πΉ quot (Xp
βf β (β Γ {π΄}))) β ((Polyββ) β
{0π})) |
96 | 92, 93, 95 | rspcdva 3614 |
. . . . . 6
β’ (π β ((degβ(πΉ quot (Xp
βf β (β Γ {π΄})))) = π· β ((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) β Fin β§
(β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) β€ (degβ(πΉ quot (Xp
βf β (β Γ {π΄}))))))) |
97 | 83, 96 | mpd 15 |
. . . . 5
β’ (π β ((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) β Fin β§
(β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) β€ (degβ(πΉ quot (Xp
βf β (β Γ {π΄})))))) |
98 | 97 | simpld 496 |
. . . 4
β’ (π β (β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) β
Fin) |
99 | | snfi 9044 |
. . . 4
β’ {π΄} β Fin |
100 | | unfi 9172 |
. . . 4
β’ (((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) β Fin β§ {π΄} β Fin) β ((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄}) β Fin) |
101 | 98, 99, 100 | sylancl 587 |
. . 3
β’ (π β ((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄}) β Fin) |
102 | 52, 101 | eqeltrd 2834 |
. 2
β’ (π β π
β Fin) |
103 | 52 | fveq2d 6896 |
. . 3
β’ (π β (β―βπ
) = (β―β((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄}))) |
104 | | hashcl 14316 |
. . . . . 6
β’ (((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄}) β Fin β (β―β((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄})) β
β0) |
105 | 101, 104 | syl 17 |
. . . . 5
β’ (π β (β―β((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄})) β
β0) |
106 | 105 | nn0red 12533 |
. . . 4
β’ (π β (β―β((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄})) β β) |
107 | | hashcl 14316 |
. . . . . . 7
β’ ((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) β Fin β
(β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) β
β0) |
108 | 98, 107 | syl 17 |
. . . . . 6
β’ (π β (β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) β
β0) |
109 | 108 | nn0red 12533 |
. . . . 5
β’ (π β (β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) β
β) |
110 | | peano2re 11387 |
. . . . 5
β’
((β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) β β β
((β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) + 1) β
β) |
111 | 109, 110 | syl 17 |
. . . 4
β’ (π β ((β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) + 1) β
β) |
112 | | dgrcl 25747 |
. . . . . 6
β’ (πΉ β (Polyββ)
β (degβπΉ) β
β0) |
113 | 4, 112 | syl 17 |
. . . . 5
β’ (π β (degβπΉ) β
β0) |
114 | 113 | nn0red 12533 |
. . . 4
β’ (π β (degβπΉ) β
β) |
115 | | hashun2 14343 |
. . . . . 6
β’ (((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) β Fin β§ {π΄} β Fin) β
(β―β((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄})) β€ ((β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) + (β―β{π΄}))) |
116 | 98, 99, 115 | sylancl 587 |
. . . . 5
β’ (π β (β―β((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄})) β€ ((β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) + (β―β{π΄}))) |
117 | | hashsng 14329 |
. . . . . . 7
β’ (π΄ β β β
(β―β{π΄}) =
1) |
118 | 11, 117 | syl 17 |
. . . . . 6
β’ (π β (β―β{π΄}) = 1) |
119 | 118 | oveq2d 7425 |
. . . . 5
β’ (π β ((β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) + (β―β{π΄})) = ((β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) + 1)) |
120 | 116, 119 | breqtrd 5175 |
. . . 4
β’ (π β (β―β((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄})) β€ ((β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) + 1)) |
121 | 57 | nn0red 12533 |
. . . . . 6
β’ (π β π· β β) |
122 | | 1red 11215 |
. . . . . 6
β’ (π β 1 β
β) |
123 | 97 | simprd 497 |
. . . . . . 7
β’ (π β (β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) β€ (degβ(πΉ quot (Xp
βf β (β Γ {π΄}))))) |
124 | 123, 83 | breqtrd 5175 |
. . . . . 6
β’ (π β (β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) β€ π·) |
125 | 109, 121,
122, 124 | leadd1dd 11828 |
. . . . 5
β’ (π β ((β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) + 1) β€ (π· + 1)) |
126 | 125, 62 | breqtrrd 5177 |
. . . 4
β’ (π β ((β―β(β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0})) + 1) β€
(degβπΉ)) |
127 | 106, 111,
114, 120, 126 | letrd 11371 |
. . 3
β’ (π β (β―β((β‘(πΉ quot (Xp
βf β (β Γ {π΄}))) β {0}) βͺ {π΄})) β€ (degβπΉ)) |
128 | 103, 127 | eqbrtrd 5171 |
. 2
β’ (π β (β―βπ
) β€ (degβπΉ)) |
129 | 102, 128 | jca 513 |
1
β’ (π β (π
β Fin β§ (β―βπ
) β€ (degβπΉ))) |