This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐺 ) ) )