plymul0or

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

		Ref	Expression
	Assertion	plymul0or	$⊢ (F \in Poly (S) \land G \in Poly (S)) \to (F \times_{f} G = 0_{𝑝} \leftrightarrow (F = 0_{𝑝} \lor G = 0_{𝑝}))$

Proof

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

Metamath Proof Explorer

Theorem plymul0or

Proof