Step | Hyp | Ref
| Expression |
1 | | plyssc 25949 |
. . 3
β’
(Polyβπ)
β (Polyββ) |
2 | 1 | sseli 3977 |
. 2
β’ (πΉ β (Polyβπ) β πΉ β
(Polyββ)) |
3 | 1 | sseli 3977 |
. . 3
β’ (πΊ β (Polyβπ) β πΊ β
(Polyββ)) |
4 | | eldifsn 4789 |
. . . . 5
β’ (πΊ β ((Polyββ)
β {0π}) β (πΊ β (Polyββ) β§ πΊ β
0π)) |
5 | | oveq1 7418 |
. . . . . . . . . . 11
β’ (π = πΊ β (π βf Β· π) = (πΊ βf Β· π)) |
6 | | oveq12 7420 |
. . . . . . . . . . 11
β’ ((π = πΉ β§ (π βf Β· π) = (πΊ βf Β· π)) β (π βf β (π βf Β·
π)) = (πΉ βf β (πΊ βf Β·
π))) |
7 | 5, 6 | sylan2 591 |
. . . . . . . . . 10
β’ ((π = πΉ β§ π = πΊ) β (π βf β (π βf Β·
π)) = (πΉ βf β (πΊ βf Β·
π))) |
8 | | quotval.1 |
. . . . . . . . . 10
β’ π
= (πΉ βf β (πΊ βf Β·
π)) |
9 | 7, 8 | eqtr4di 2788 |
. . . . . . . . 9
β’ ((π = πΉ β§ π = πΊ) β (π βf β (π βf Β·
π)) = π
) |
10 | 9 | sbceq1d 3781 |
. . . . . . . 8
β’ ((π = πΉ β§ π = πΊ) β ([(π βf β (π βf Β·
π)) / π](π = 0π β¨
(degβπ) <
(degβπ)) β
[π
/ π](π = 0π β¨
(degβπ) <
(degβπ)))) |
11 | 8 | ovexi 7445 |
. . . . . . . . . 10
β’ π
β V |
12 | | eqeq1 2734 |
. . . . . . . . . . 11
β’ (π = π
β (π = 0π β π
=
0π)) |
13 | | fveq2 6890 |
. . . . . . . . . . . 12
β’ (π = π
β (degβπ) = (degβπ
)) |
14 | 13 | breq1d 5157 |
. . . . . . . . . . 11
β’ (π = π
β ((degβπ) < (degβπ) β (degβπ
) < (degβπ))) |
15 | 12, 14 | orbi12d 915 |
. . . . . . . . . 10
β’ (π = π
β ((π = 0π β¨
(degβπ) <
(degβπ)) β
(π
= 0π
β¨ (degβπ
) <
(degβπ)))) |
16 | 11, 15 | sbcie 3819 |
. . . . . . . . 9
β’
([π
/ π](π = 0π β¨
(degβπ) <
(degβπ)) β
(π
= 0π
β¨ (degβπ
) <
(degβπ))) |
17 | | simpr 483 |
. . . . . . . . . . . 12
β’ ((π = πΉ β§ π = πΊ) β π = πΊ) |
18 | 17 | fveq2d 6894 |
. . . . . . . . . . 11
β’ ((π = πΉ β§ π = πΊ) β (degβπ) = (degβπΊ)) |
19 | 18 | breq2d 5159 |
. . . . . . . . . 10
β’ ((π = πΉ β§ π = πΊ) β ((degβπ
) < (degβπ) β (degβπ
) < (degβπΊ))) |
20 | 19 | orbi2d 912 |
. . . . . . . . 9
β’ ((π = πΉ β§ π = πΊ) β ((π
= 0π β¨
(degβπ
) <
(degβπ)) β
(π
= 0π
β¨ (degβπ
) <
(degβπΊ)))) |
21 | 16, 20 | bitrid 282 |
. . . . . . . 8
β’ ((π = πΉ β§ π = πΊ) β ([π
/ π](π = 0π β¨
(degβπ) <
(degβπ)) β
(π
= 0π
β¨ (degβπ
) <
(degβπΊ)))) |
22 | 10, 21 | bitrd 278 |
. . . . . . 7
β’ ((π = πΉ β§ π = πΊ) β ([(π βf β (π βf Β·
π)) / π](π = 0π β¨
(degβπ) <
(degβπ)) β
(π
= 0π
β¨ (degβπ
) <
(degβπΊ)))) |
23 | 22 | riotabidv 7369 |
. . . . . 6
β’ ((π = πΉ β§ π = πΊ) β (β©π β (Polyββ)[(π βf β
(π βf
Β· π)) / π](π = 0π β¨
(degβπ) <
(degβπ))) =
(β©π β
(Polyββ)(π
=
0π β¨ (degβπ
) < (degβπΊ)))) |
24 | | df-quot 26040 |
. . . . . 6
β’ quot =
(π β
(Polyββ), π
β ((Polyββ) β {0π}) β¦
(β©π β
(Polyββ)[(π βf β (π βf Β·
π)) / π](π = 0π β¨
(degβπ) <
(degβπ)))) |
25 | | riotaex 7371 |
. . . . . 6
β’
(β©π
β (Polyββ)(π
= 0π β¨
(degβπ
) <
(degβπΊ))) β
V |
26 | 23, 24, 25 | ovmpoa 7565 |
. . . . 5
β’ ((πΉ β (Polyββ)
β§ πΊ β
((Polyββ) β {0π})) β (πΉ quot πΊ) = (β©π β (Polyββ)(π
= 0π β¨
(degβπ
) <
(degβπΊ)))) |
27 | 4, 26 | sylan2br 593 |
. . . 4
β’ ((πΉ β (Polyββ)
β§ (πΊ β
(Polyββ) β§ πΊ β 0π)) β (πΉ quot πΊ) = (β©π β (Polyββ)(π
= 0π β¨
(degβπ
) <
(degβπΊ)))) |
28 | 27 | 3impb 1113 |
. . 3
β’ ((πΉ β (Polyββ)
β§ πΊ β
(Polyββ) β§ πΊ β 0π) β (πΉ quot πΊ) = (β©π β (Polyββ)(π
= 0π β¨
(degβπ
) <
(degβπΊ)))) |
29 | 3, 28 | syl3an2 1162 |
. 2
β’ ((πΉ β (Polyββ)
β§ πΊ β
(Polyβπ) β§ πΊ β 0π)
β (πΉ quot πΊ) = (β©π β
(Polyββ)(π
=
0π β¨ (degβπ
) < (degβπΊ)))) |
30 | 2, 29 | syl3an1 1161 |
1
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ πΊ β 0π) β (πΉ quot πΊ) = (β©π β (Polyββ)(π
= 0π β¨
(degβπ
) <
(degβπΊ)))) |