Step | Hyp | Ref
| Expression |
1 | | fveq2 6825 |
. . 3
β’ (πΉ = πΊ β (coeffβπΉ) = (coeffβπΊ)) |
2 | | coefv0.1 |
. . 3
β’ π΄ = (coeffβπΉ) |
3 | | coeadd.2 |
. . 3
β’ π΅ = (coeffβπΊ) |
4 | 1, 2, 3 | 3eqtr4g 2801 |
. 2
β’ (πΉ = πΊ β π΄ = π΅) |
5 | | simp3 1137 |
. . . . . . . . . . 11
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β π΄ = π΅) |
6 | 5 | cnveqd 5817 |
. . . . . . . . . 10
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β β‘π΄ = β‘π΅) |
7 | 6 | imaeq1d 5998 |
. . . . . . . . 9
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β (β‘π΄ β (β β {0})) = (β‘π΅ β (β β
{0}))) |
8 | 7 | supeq1d 9303 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β sup((β‘π΄ β (β β {0})),
β0, < ) = sup((β‘π΅ β (β β {0})),
β0, < )) |
9 | 2 | dgrval 25495 |
. . . . . . . . 9
β’ (πΉ β (Polyβπ) β (degβπΉ) = sup((β‘π΄ β (β β {0})),
β0, < )) |
10 | 9 | 3ad2ant1 1132 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β (degβπΉ) = sup((β‘π΄ β (β β {0})),
β0, < )) |
11 | 3 | dgrval 25495 |
. . . . . . . . 9
β’ (πΊ β (Polyβπ) β (degβπΊ) = sup((β‘π΅ β (β β {0})),
β0, < )) |
12 | 11 | 3ad2ant2 1133 |
. . . . . . . 8
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β (degβπΊ) = sup((β‘π΅ β (β β {0})),
β0, < )) |
13 | 8, 10, 12 | 3eqtr4d 2786 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β (degβπΉ) = (degβπΊ)) |
14 | 13 | oveq2d 7353 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β (0...(degβπΉ)) = (0...(degβπΊ))) |
15 | | simpl3 1192 |
. . . . . . . 8
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β§ π β (0...(degβπΉ))) β π΄ = π΅) |
16 | 15 | fveq1d 6827 |
. . . . . . 7
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β§ π β (0...(degβπΉ))) β (π΄βπ) = (π΅βπ)) |
17 | 16 | oveq1d 7352 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β§ π β (0...(degβπΉ))) β ((π΄βπ) Β· (π§βπ)) = ((π΅βπ) Β· (π§βπ))) |
18 | 14, 17 | sumeq12dv 15517 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β Ξ£π β (0...(degβπΉ))((π΄βπ) Β· (π§βπ)) = Ξ£π β (0...(degβπΊ))((π΅βπ) Β· (π§βπ))) |
19 | 18 | mpteq2dv 5194 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β (π§ β β β¦ Ξ£π β (0...(degβπΉ))((π΄βπ) Β· (π§βπ))) = (π§ β β β¦ Ξ£π β (0...(degβπΊ))((π΅βπ) Β· (π§βπ)))) |
20 | | eqid 2736 |
. . . . . 6
β’
(degβπΉ) =
(degβπΉ) |
21 | 2, 20 | coeid 25505 |
. . . . 5
β’ (πΉ β (Polyβπ) β πΉ = (π§ β β β¦ Ξ£π β (0...(degβπΉ))((π΄βπ) Β· (π§βπ)))) |
22 | 21 | 3ad2ant1 1132 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β πΉ = (π§ β β β¦ Ξ£π β (0...(degβπΉ))((π΄βπ) Β· (π§βπ)))) |
23 | | eqid 2736 |
. . . . . 6
β’
(degβπΊ) =
(degβπΊ) |
24 | 3, 23 | coeid 25505 |
. . . . 5
β’ (πΊ β (Polyβπ) β πΊ = (π§ β β β¦ Ξ£π β (0...(degβπΊ))((π΅βπ) Β· (π§βπ)))) |
25 | 24 | 3ad2ant2 1133 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β πΊ = (π§ β β β¦ Ξ£π β (0...(degβπΊ))((π΅βπ) Β· (π§βπ)))) |
26 | 19, 22, 25 | 3eqtr4d 2786 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ) β§ π΄ = π΅) β πΉ = πΊ) |
27 | 26 | 3expia 1120 |
. 2
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (π΄ = π΅ β πΉ = πΊ)) |
28 | 4, 27 | impbid2 225 |
1
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (πΉ = πΊ β π΄ = π΅)) |