Step | Hyp | Ref
| Expression |
1 | | dgrcl 25983 |
. . . . . . 7
β’ (πΉ β (Polyβπ) β (degβπΉ) β
β0) |
2 | | dgrcl 25983 |
. . . . . . 7
β’ (πΊ β (Polyβπ) β (degβπΊ) β
β0) |
3 | | nn0addcl 12512 |
. . . . . . 7
β’
(((degβπΉ)
β β0 β§ (degβπΊ) β β0) β
((degβπΉ) +
(degβπΊ)) β
β0) |
4 | 1, 2, 3 | syl2an 595 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((degβπΉ) + (degβπΊ)) β
β0) |
5 | | c0ex 11213 |
. . . . . . 7
β’ 0 β
V |
6 | 5 | fvconst2 7207 |
. . . . . 6
β’
(((degβπΉ) +
(degβπΊ)) β
β0 β ((β0 Γ
{0})β((degβπΉ) +
(degβπΊ))) =
0) |
7 | 4, 6 | syl 17 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((β0 Γ
{0})β((degβπΉ) +
(degβπΊ))) =
0) |
8 | | fveq2 6891 |
. . . . . . . 8
β’ ((πΉ βf Β·
πΊ) = 0π
β (coeffβ(πΉ
βf Β· πΊ)) =
(coeffβ0π)) |
9 | | coe0 26006 |
. . . . . . . 8
β’
(coeffβ0π) = (β0 Γ
{0}) |
10 | 8, 9 | eqtrdi 2787 |
. . . . . . 7
β’ ((πΉ βf Β·
πΊ) = 0π
β (coeffβ(πΉ
βf Β· πΊ)) = (β0 Γ
{0})) |
11 | 10 | fveq1d 6893 |
. . . . . 6
β’ ((πΉ βf Β·
πΊ) = 0π
β ((coeffβ(πΉ
βf Β· πΊ))β((degβπΉ) + (degβπΊ))) = ((β0 Γ
{0})β((degβπΉ) +
(degβπΊ)))) |
12 | 11 | eqeq1d 2733 |
. . . . 5
β’ ((πΉ βf Β·
πΊ) = 0π
β (((coeffβ(πΉ
βf Β· πΊ))β((degβπΉ) + (degβπΊ))) = 0 β ((β0 Γ
{0})β((degβπΉ) +
(degβπΊ))) =
0)) |
13 | 7, 12 | syl5ibrcom 246 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((πΉ βf Β· πΊ) = 0π β
((coeffβ(πΉ
βf Β· πΊ))β((degβπΉ) + (degβπΊ))) = 0)) |
14 | | eqid 2731 |
. . . . . . 7
β’
(coeffβπΉ) =
(coeffβπΉ) |
15 | | eqid 2731 |
. . . . . . 7
β’
(coeffβπΊ) =
(coeffβπΊ) |
16 | | eqid 2731 |
. . . . . . 7
β’
(degβπΉ) =
(degβπΉ) |
17 | | eqid 2731 |
. . . . . . 7
β’
(degβπΊ) =
(degβπΊ) |
18 | 14, 15, 16, 17 | coemulhi 26004 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((coeffβ(πΉ βf Β· πΊ))β((degβπΉ) + (degβπΊ))) = (((coeffβπΉ)β(degβπΉ)) Β· ((coeffβπΊ)β(degβπΊ)))) |
19 | 18 | eqeq1d 2733 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (((coeffβ(πΉ βf Β· πΊ))β((degβπΉ) + (degβπΊ))) = 0 β (((coeffβπΉ)β(degβπΉ)) Β· ((coeffβπΊ)β(degβπΊ))) = 0)) |
20 | 14 | coef3 25982 |
. . . . . . . 8
β’ (πΉ β (Polyβπ) β (coeffβπΉ):β0βΆβ) |
21 | 20 | adantr 480 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (coeffβπΉ):β0βΆβ) |
22 | 1 | adantr 480 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (degβπΉ) β
β0) |
23 | 21, 22 | ffvelcdmd 7087 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((coeffβπΉ)β(degβπΉ)) β β) |
24 | 15 | coef3 25982 |
. . . . . . . 8
β’ (πΊ β (Polyβπ) β (coeffβπΊ):β0βΆβ) |
25 | 24 | adantl 481 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (coeffβπΊ):β0βΆβ) |
26 | 2 | adantl 481 |
. . . . . . 7
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (degβπΊ) β
β0) |
27 | 25, 26 | ffvelcdmd 7087 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((coeffβπΊ)β(degβπΊ)) β β) |
28 | 23, 27 | mul0ord 11869 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((((coeffβπΉ)β(degβπΉ)) Β· ((coeffβπΊ)β(degβπΊ))) = 0 β (((coeffβπΉ)β(degβπΉ)) = 0 β¨ ((coeffβπΊ)β(degβπΊ)) = 0))) |
29 | 19, 28 | bitrd 279 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (((coeffβ(πΉ βf Β· πΊ))β((degβπΉ) + (degβπΊ))) = 0 β (((coeffβπΉ)β(degβπΉ)) = 0 β¨ ((coeffβπΊ)β(degβπΊ)) = 0))) |
30 | 13, 29 | sylibd 238 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((πΉ βf Β· πΊ) = 0π β
(((coeffβπΉ)β(degβπΉ)) = 0 β¨ ((coeffβπΊ)β(degβπΊ)) = 0))) |
31 | 16, 14 | dgreq0 26016 |
. . . . 5
β’ (πΉ β (Polyβπ) β (πΉ = 0π β
((coeffβπΉ)β(degβπΉ)) = 0)) |
32 | 31 | adantr 480 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (πΉ = 0π β
((coeffβπΉ)β(degβπΉ)) = 0)) |
33 | 17, 15 | dgreq0 26016 |
. . . . 5
β’ (πΊ β (Polyβπ) β (πΊ = 0π β
((coeffβπΊ)β(degβπΊ)) = 0)) |
34 | 33 | adantl 481 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (πΊ = 0π β
((coeffβπΊ)β(degβπΊ)) = 0)) |
35 | 32, 34 | orbi12d 916 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((πΉ = 0π β¨ πΊ = 0π) β
(((coeffβπΉ)β(degβπΉ)) = 0 β¨ ((coeffβπΊ)β(degβπΊ)) = 0))) |
36 | 30, 35 | sylibrd 259 |
. 2
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((πΉ βf Β· πΊ) = 0π β
(πΉ = 0π
β¨ πΊ =
0π))) |
37 | | cnex 11195 |
. . . . . . 7
β’ β
β V |
38 | 37 | a1i 11 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β β β V) |
39 | | plyf 25948 |
. . . . . . 7
β’ (πΊ β (Polyβπ) β πΊ:ββΆβ) |
40 | 39 | adantl 481 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β πΊ:ββΆβ) |
41 | | 0cnd 11212 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β 0 β β) |
42 | | mul02 11397 |
. . . . . . 7
β’ (π₯ β β β (0
Β· π₯) =
0) |
43 | 42 | adantl 481 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π₯ β β) β (0 Β· π₯) = 0) |
44 | 38, 40, 41, 41, 43 | caofid2 7708 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((β Γ {0})
βf Β· πΊ) = (β Γ {0})) |
45 | | id 22 |
. . . . . . . 8
β’ (πΉ = 0π β
πΉ =
0π) |
46 | | df-0p 25420 |
. . . . . . . 8
β’
0π = (β Γ {0}) |
47 | 45, 46 | eqtrdi 2787 |
. . . . . . 7
β’ (πΉ = 0π β
πΉ = (β Γ
{0})) |
48 | 47 | oveq1d 7427 |
. . . . . 6
β’ (πΉ = 0π β
(πΉ βf
Β· πΊ) = ((β
Γ {0}) βf Β· πΊ)) |
49 | 48 | eqeq1d 2733 |
. . . . 5
β’ (πΉ = 0π β
((πΉ βf
Β· πΊ) = (β
Γ {0}) β ((β Γ {0}) βf Β· πΊ) = (β Γ
{0}))) |
50 | 44, 49 | syl5ibrcom 246 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (πΉ = 0π β (πΉ βf Β·
πΊ) = (β Γ
{0}))) |
51 | | plyf 25948 |
. . . . . . 7
β’ (πΉ β (Polyβπ) β πΉ:ββΆβ) |
52 | 51 | adantr 480 |
. . . . . 6
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β πΉ:ββΆβ) |
53 | | mul01 11398 |
. . . . . . 7
β’ (π₯ β β β (π₯ Β· 0) =
0) |
54 | 53 | adantl 481 |
. . . . . 6
β’ (((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β§ π₯ β β) β (π₯ Β· 0) = 0) |
55 | 38, 52, 41, 41, 54 | caofid1 7707 |
. . . . 5
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (πΉ βf Β· (β
Γ {0})) = (β Γ {0})) |
56 | | id 22 |
. . . . . . . 8
β’ (πΊ = 0π β
πΊ =
0π) |
57 | 56, 46 | eqtrdi 2787 |
. . . . . . 7
β’ (πΊ = 0π β
πΊ = (β Γ
{0})) |
58 | 57 | oveq2d 7428 |
. . . . . 6
β’ (πΊ = 0π β
(πΉ βf
Β· πΊ) = (πΉ βf Β·
(β Γ {0}))) |
59 | 58 | eqeq1d 2733 |
. . . . 5
β’ (πΊ = 0π β
((πΉ βf
Β· πΊ) = (β
Γ {0}) β (πΉ
βf Β· (β Γ {0})) = (β Γ
{0}))) |
60 | 55, 59 | syl5ibrcom 246 |
. . . 4
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β (πΊ = 0π β (πΉ βf Β·
πΊ) = (β Γ
{0}))) |
61 | 50, 60 | jaod 856 |
. . 3
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((πΉ = 0π β¨ πΊ = 0π) β
(πΉ βf
Β· πΊ) = (β
Γ {0}))) |
62 | 46 | eqeq2i 2744 |
. . 3
β’ ((πΉ βf Β·
πΊ) = 0π
β (πΉ
βf Β· πΊ) = (β Γ {0})) |
63 | 61, 62 | imbitrrdi 251 |
. 2
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((πΉ = 0π β¨ πΊ = 0π) β
(πΉ βf
Β· πΊ) =
0π)) |
64 | 36, 63 | impbid 211 |
1
β’ ((πΉ β (Polyβπ) β§ πΊ β (Polyβπ)) β ((πΉ βf Β· πΊ) = 0π β
(πΉ = 0π
β¨ πΊ =
0π))) |