Metamath Proof Explorer


Theorem plymul0or

Description: Polynomial multiplication has no zero divisors. (Contributed by Mario Carneiro, 26-Jul-2014)

Ref Expression
Assertion plymul0or F Poly S G Poly S F × f G = 0 𝑝 F = 0 𝑝 G = 0 𝑝

Proof

Step Hyp Ref Expression
1 dgrcl F Poly S deg F 0
2 dgrcl G Poly S deg G 0
3 nn0addcl deg F 0 deg G 0 deg F + deg G 0
4 1 2 3 syl2an F Poly S G Poly S deg F + deg G 0
5 c0ex 0 V
6 5 fvconst2 deg F + deg G 0 0 × 0 deg F + deg G = 0
7 4 6 syl F Poly S G Poly S 0 × 0 deg F + deg G = 0
8 fveq2 F × f G = 0 𝑝 coeff F × f G = coeff 0 𝑝
9 coe0 coeff 0 𝑝 = 0 × 0
10 8 9 eqtrdi F × f G = 0 𝑝 coeff F × f G = 0 × 0
11 10 fveq1d F × f G = 0 𝑝 coeff F × f G deg F + deg G = 0 × 0 deg F + deg G
12 11 eqeq1d F × f G = 0 𝑝 coeff F × f G deg F + deg G = 0 0 × 0 deg F + deg G = 0
13 7 12 syl5ibrcom F Poly S G Poly S F × f G = 0 𝑝 coeff F × f G deg F + deg G = 0
14 eqid coeff F = coeff F
15 eqid coeff G = coeff G
16 eqid deg F = deg F
17 eqid deg G = deg G
18 14 15 16 17 coemulhi F Poly S G Poly S coeff F × f G deg F + deg G = coeff F deg F coeff G deg G
19 18 eqeq1d F Poly S G Poly S coeff F × f G deg F + deg G = 0 coeff F deg F coeff G deg G = 0
20 14 coef3 F Poly S coeff F : 0
21 20 adantr F Poly S G Poly S coeff F : 0
22 1 adantr F Poly S G Poly S deg F 0
23 21 22 ffvelrnd F Poly S G Poly S coeff F deg F
24 15 coef3 G Poly S coeff G : 0
25 24 adantl F Poly S G Poly S coeff G : 0
26 2 adantl F Poly S G Poly S deg G 0
27 25 26 ffvelrnd F Poly S G Poly S coeff G deg G
28 23 27 mul0ord F Poly S G Poly S coeff F deg F coeff G deg G = 0 coeff F deg F = 0 coeff G deg G = 0
29 19 28 bitrd F Poly S G Poly S coeff F × f G deg F + deg G = 0 coeff F deg F = 0 coeff G deg G = 0
30 13 29 sylibd F Poly S G Poly S F × f G = 0 𝑝 coeff F deg F = 0 coeff G deg G = 0
31 16 14 dgreq0 F Poly S F = 0 𝑝 coeff F deg F = 0
32 31 adantr F Poly S G Poly S F = 0 𝑝 coeff F deg F = 0
33 17 15 dgreq0 G Poly S G = 0 𝑝 coeff G deg G = 0
34 33 adantl F Poly S G Poly S G = 0 𝑝 coeff G deg G = 0
35 32 34 orbi12d F Poly S G Poly S F = 0 𝑝 G = 0 𝑝 coeff F deg F = 0 coeff G deg G = 0
36 30 35 sylibrd F Poly S G Poly S F × f G = 0 𝑝 F = 0 𝑝 G = 0 𝑝
37 cnex V
38 37 a1i F Poly S G Poly S V
39 plyf G Poly S G :
40 39 adantl F Poly S G Poly S G :
41 0cnd F Poly S G Poly S 0
42 mul02 x 0 x = 0
43 42 adantl F Poly S G Poly S x 0 x = 0
44 38 40 41 41 43 caofid2 F Poly S G Poly S × 0 × f G = × 0
45 id F = 0 𝑝 F = 0 𝑝
46 df-0p 0 𝑝 = × 0
47 45 46 eqtrdi F = 0 𝑝 F = × 0
48 47 oveq1d F = 0 𝑝 F × f G = × 0 × f G
49 48 eqeq1d F = 0 𝑝 F × f G = × 0 × 0 × f G = × 0
50 44 49 syl5ibrcom F Poly S G Poly S F = 0 𝑝 F × f G = × 0
51 plyf F Poly S F :
52 51 adantr F Poly S G Poly S F :
53 mul01 x x 0 = 0
54 53 adantl F Poly S G Poly S x x 0 = 0
55 38 52 41 41 54 caofid1 F Poly S G Poly S F × f × 0 = × 0
56 id G = 0 𝑝 G = 0 𝑝
57 56 46 eqtrdi G = 0 𝑝 G = × 0
58 57 oveq2d G = 0 𝑝 F × f G = F × f × 0
59 58 eqeq1d G = 0 𝑝 F × f G = × 0 F × f × 0 = × 0
60 55 59 syl5ibrcom F Poly S G Poly S G = 0 𝑝 F × f G = × 0
61 50 60 jaod F Poly S G Poly S F = 0 𝑝 G = 0 𝑝 F × f G = × 0
62 46 eqeq2i F × f G = 0 𝑝 F × f G = × 0
63 61 62 syl6ibr F Poly S G Poly S F = 0 𝑝 G = 0 𝑝 F × f G = 0 𝑝
64 36 63 impbid F Poly S G Poly S F × f G = 0 𝑝 F = 0 𝑝 G = 0 𝑝