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 ffvelcdmd ⊢ ( ( 𝐹 ∈ ( 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 ffvelcdmd ⊢ ( ( 𝐹 ∈ ( 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 imbitrrdi ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐹 = 0𝑝 ∨ 𝐺 = 0𝑝 ) → ( 𝐹 ∘f · 𝐺 ) = 0𝑝 ) )
64 36 63 impbid ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( ( 𝐹 ∘f · 𝐺 ) = 0𝑝 ↔ ( 𝐹 = 0𝑝 ∨ 𝐺 = 0𝑝 ) ) )