Metamath Proof Explorer


Theorem plymul0or

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

Ref Expression
Assertion plymul0or ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐹f · 𝐺 ) = 0𝑝 ↔ ( 𝐹 = 0𝑝𝐺 = 0𝑝 ) ) )

Proof

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