facth

Description: The factor theorem. If a polynomial F has a root at A , then G = x - A is a factor of F (and the other factor is F quot G ). This is part of Metamath 100 proof #89. (Contributed by Mario Carneiro, 26-Jul-2014)

		Ref	Expression
	Hypothesis	facth.1	$⊢ G = X^{p} -_{f} (ℂ \times \{A\})$
	Assertion	facth	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to F = G \times_{f} (F quot G)$

Proof

Step	Hyp	Ref	Expression
1		facth.1	$⊢ G = X^{p} -_{f} (ℂ \times \{A\})$
2		eqid	$⊢ F -_{f} (G \times_{f} (F quot G)) = F -_{f} (G \times_{f} (F quot G))$
3	1 2	plyrem	$⊢ (F \in Poly (S) \land A \in ℂ) \to F -_{f} (G \times_{f} (F quot G)) = ℂ \times \{F (A)\}$
4	3	3adant3	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to F -_{f} (G \times_{f} (F quot G)) = ℂ \times \{F (A)\}$
5		simp3	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to F (A) = 0$
6	5	sneqd	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to \{F (A)\} = \{0\}$
7	6	xpeq2d	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to ℂ \times \{F (A)\} = ℂ \times \{0\}$
8	4 7	eqtrd	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to F -_{f} (G \times_{f} (F quot G)) = ℂ \times \{0\}$
9		cnex	$⊢ ℂ \in V$
10	9	a1i	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to ℂ \in V$
11		simp1	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to F \in Poly (S)$
12		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
13	11 12	syl	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to F : ℂ ⟶ ℂ$
14	1	plyremlem	$⊢ A \in ℂ \to (G \in Poly (ℂ) \land \deg (G) = 1 \land G^{-1} [\{0\}] = \{A\})$
15	14	3ad2ant2	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to (G \in Poly (ℂ) \land \deg (G) = 1 \land G^{-1} [\{0\}] = \{A\})$
16	15	simp1d	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to G \in Poly (ℂ)$
17		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
18	17 11	sselid	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to F \in Poly (ℂ)$
19	15	simp2d	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to \deg (G) = 1$
20		ax-1ne0	$⊢ 1 \neq 0$
21	20	a1i	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to 1 \neq 0$
22	19 21	eqnetrd	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to \deg (G) \neq 0$
23		fveq2	$⊢ G = 0_{𝑝} \to \deg (G) = \deg (0_{𝑝})$
24		dgr0	$⊢ \deg (0_{𝑝}) = 0$
25	23 24	eqtrdi	$⊢ G = 0_{𝑝} \to \deg (G) = 0$
26	25	necon3i	$⊢ \deg (G) \neq 0 \to G \neq 0_{𝑝}$
27	22 26	syl	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to G \neq 0_{𝑝}$
28		quotcl2	$⊢ (F \in Poly (ℂ) \land G \in Poly (ℂ) \land G \neq 0_{𝑝}) \to F quot G \in Poly (ℂ)$
29	18 16 27 28	syl3anc	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to F quot G \in Poly (ℂ)$
30		plymulcl	$⊢ (G \in Poly (ℂ) \land F quot G \in Poly (ℂ)) \to G \times_{f} (F quot G) \in Poly (ℂ)$
31	16 29 30	syl2anc	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to G \times_{f} (F quot G) \in Poly (ℂ)$
32		plyf	$⊢ G \times_{f} (F quot G) \in Poly (ℂ) \to (G \times_{f} (F quot G)) : ℂ ⟶ ℂ$
33	31 32	syl	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to (G \times_{f} (F quot G)) : ℂ ⟶ ℂ$
34		ofsubeq0	$⊢ (ℂ \in V \land F : ℂ ⟶ ℂ \land (G \times_{f} (F quot G)) : ℂ ⟶ ℂ) \to (F -_{f} (G \times_{f} (F quot G)) = ℂ \times \{0\} \leftrightarrow F = G \times_{f} (F quot G))$
35	10 13 33 34	syl3anc	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to (F -_{f} (G \times_{f} (F quot G)) = ℂ \times \{0\} \leftrightarrow F = G \times_{f} (F quot G))$
36	8 35	mpbid	$⊢ (F \in Poly (S) \land A \in ℂ \land F (A) = 0) \to F = G \times_{f} (F quot G)$

Metamath Proof Explorer

Theorem facth

Proof