Theorem 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	⊢ 𝐺 = ( Xp ∘f − ( ℂ × { 𝐴 } ) )
Assertion	facth	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐹 = ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		facth.1	⊢ 𝐺 = ( Xp ∘f − ( ℂ × { 𝐴 } ) )
2		eqid	⊢ ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) = ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) )
3	1 2	plyrem	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ) → ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) = ( ℂ × { ( 𝐹 ‘ 𝐴 ) } ) )
4	3	3adant3	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) = ( ℂ × { ( 𝐹 ‘ 𝐴 ) } ) )
5		simp3	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ( 𝐹 ‘ 𝐴 ) = 0 )
6	5	sneqd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → { ( 𝐹 ‘ 𝐴 ) } = { 0 } )
7	6	xpeq2d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ( ℂ × { ( 𝐹 ‘ 𝐴 ) } ) = ( ℂ × { 0 } ) )
8	4 7	eqtrd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) = ( ℂ × { 0 } ) )
9		cnex	⊢ ℂ ∈ V
10	9	a1i	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ℂ ∈ V )
11		simp1	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
12		plyf	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
13	11 12	syl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐹 : ℂ ⟶ ℂ )
14	1	plyremlem	⊢ ( 𝐴 ∈ ℂ → ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝐺 ) = 1 ∧ ( ◡ 𝐺 “ { 0 } ) = { 𝐴 } ) )
15	14	3ad2ant2	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ ( deg ‘ 𝐺 ) = 1 ∧ ( ◡ 𝐺 “ { 0 } ) = { 𝐴 } ) )
16	15	simp1d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐺 ∈ ( Poly ‘ ℂ ) )
17		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
18	17 11	sselid	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
19	15	simp2d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ( deg ‘ 𝐺 ) = 1 )
20		ax-1ne0	⊢ 1 ≠ 0
21	20	a1i	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 1 ≠ 0 )
22	19 21	eqnetrd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ( deg ‘ 𝐺 ) ≠ 0 )
23		fveq2	⊢ ( 𝐺 = 0𝑝 → ( deg ‘ 𝐺 ) = ( deg ‘ 0𝑝 ) )
24		dgr0	⊢ ( deg ‘ 0𝑝 ) = 0
25	23 24	eqtrdi	⊢ ( 𝐺 = 0𝑝 → ( deg ‘ 𝐺 ) = 0 )
26	25	necon3i	⊢ ( ( deg ‘ 𝐺 ) ≠ 0 → 𝐺 ≠ 0𝑝 )
27	22 26	syl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐺 ≠ 0𝑝 )
28		quotcl2	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 quot 𝐺 ) ∈ ( Poly ‘ ℂ ) )
29	18 16 27 28	syl3anc	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ( 𝐹 quot 𝐺 ) ∈ ( Poly ‘ ℂ ) )
30		plymulcl	⊢ ( ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ ( 𝐹 quot 𝐺 ) ∈ ( Poly ‘ ℂ ) ) → ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) )
31	16 29 30	syl2anc	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) )
32		plyf	⊢ ( ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) → ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) : ℂ ⟶ ℂ )
33	31 32	syl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) : ℂ ⟶ ℂ )
34		ofsubeq0	⊢ ( ( ℂ ∈ V ∧ 𝐹 : ℂ ⟶ ℂ ∧ ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) : ℂ ⟶ ℂ ) → ( ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) = ( ℂ × { 0 } ) ↔ 𝐹 = ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) )
35	10 13 33 34	syl3anc	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → ( ( 𝐹 ∘f − ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) = ( ℂ × { 0 } ) ↔ 𝐹 = ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) ) )
36	8 35	mpbid	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐴 ∈ ℂ ∧ ( 𝐹 ‘ 𝐴 ) = 0 ) → 𝐹 = ( 𝐺 ∘f · ( 𝐹 quot 𝐺 ) ) )