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

Metamath Proof Explorer

Theorem facth1

Description: The factor theorem and its converse. A polynomial F has a root at A iff G = x - A is a factor of F . (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses ply1rem.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
ply1rem.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
ply1rem.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
ply1rem.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
ply1rem.m ⊢ − = ( -g ‘ 𝑃 )
ply1rem.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
ply1rem.g ⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 𝑁 ) )
ply1rem.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
ply1rem.1 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
ply1rem.2 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
ply1rem.3 ⊢ ( 𝜑 → 𝑁 ∈ 𝐾 )
ply1rem.4 ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
facth1.z ⊢ 0 = ( 0g ‘ 𝑅 )
facth1.d ⊢ ∥ = ( ∥r ‘ 𝑃 )
Assertion facth1 ( 𝜑 → ( 𝐺 ∥ 𝐹 ↔ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 ply1rem.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 ply1rem.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
3 ply1rem.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
4 ply1rem.x ⊢ 𝑋 = ( var1 ‘ 𝑅 )
5 ply1rem.m ⊢ − = ( -g ‘ 𝑃 )
6 ply1rem.a ⊢ 𝐴 = ( algSc ‘ 𝑃 )
7 ply1rem.g ⊢ 𝐺 = ( 𝑋 − ( 𝐴 ‘ 𝑁 ) )
8 ply1rem.o ⊢ 𝑂 = ( eval1 ‘ 𝑅 )
9 ply1rem.1 ⊢ ( 𝜑 → 𝑅 ∈ NzRing )
10 ply1rem.2 ⊢ ( 𝜑 → 𝑅 ∈ CRing )
11 ply1rem.3 ⊢ ( 𝜑 → 𝑁 ∈ 𝐾 )
12 ply1rem.4 ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
13 facth1.z ⊢ 0 = ( 0g ‘ 𝑅 )
14 facth1.d ⊢ ∥ = ( ∥r ‘ 𝑃 )
15 nzrring ⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )
16 9 15 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
17 eqid ⊢ ( Monic1p ‘ 𝑅 ) = ( Monic1p ‘ 𝑅 )
18 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
19 1 2 3 4 5 6 7 8 9 10 11 17 18 13 ply1remlem ⊢ ( 𝜑 → ( 𝐺 ∈ ( Monic1p ‘ 𝑅 ) ∧ ( ( deg1 ‘ 𝑅 ) ‘ 𝐺 ) = 1 ∧ ( ◡ ( 𝑂 ‘ 𝐺 ) “ { 0 } ) = { 𝑁 } ) )
20 19 simp1d ⊢ ( 𝜑 → 𝐺 ∈ ( Monic1p ‘ 𝑅 ) )
21 eqid ⊢ ( Unic1p ‘ 𝑅 ) = ( Unic1p ‘ 𝑅 )
22 21 17 mon1puc1p ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐺 ∈ ( Monic1p ‘ 𝑅 ) ) → 𝐺 ∈ ( Unic1p ‘ 𝑅 ) )
23 16 20 22 syl2anc ⊢ ( 𝜑 → 𝐺 ∈ ( Unic1p ‘ 𝑅 ) )
24 eqid ⊢ ( 0g ‘ 𝑃 ) = ( 0g ‘ 𝑃 )
25 eqid ⊢ ( rem1p ‘ 𝑅 ) = ( rem1p ‘ 𝑅 )
26 1 14 2 21 24 25 dvdsr1p ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐹 ∈ 𝐵 ∧ 𝐺 ∈ ( Unic1p ‘ 𝑅 ) ) → ( 𝐺 ∥ 𝐹 ↔ ( 𝐹 ( rem1p ‘ 𝑅 ) 𝐺 ) = ( 0g ‘ 𝑃 ) ) )
27 16 12 23 26 syl3anc ⊢ ( 𝜑 → ( 𝐺 ∥ 𝐹 ↔ ( 𝐹 ( rem1p ‘ 𝑅 ) 𝐺 ) = ( 0g ‘ 𝑃 ) ) )
28 1 2 3 4 5 6 7 8 9 10 11 12 25 ply1rem ⊢ ( 𝜑 → ( 𝐹 ( rem1p ‘ 𝑅 ) 𝐺 ) = ( 𝐴 ‘ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) ) )
29 1 6 13 24 ply1scl0 ⊢ ( 𝑅 ∈ Ring → ( 𝐴 ‘ 0 ) = ( 0g ‘ 𝑃 ) )
30 16 29 syl ⊢ ( 𝜑 → ( 𝐴 ‘ 0 ) = ( 0g ‘ 𝑃 ) )
31 30 eqcomd ⊢ ( 𝜑 → ( 0g ‘ 𝑃 ) = ( 𝐴 ‘ 0 ) )
32 28 31 eqeq12d ⊢ ( 𝜑 → ( ( 𝐹 ( rem1p ‘ 𝑅 ) 𝐺 ) = ( 0g ‘ 𝑃 ) ↔ ( 𝐴 ‘ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) ) = ( 𝐴 ‘ 0 ) ) )
33 1 6 3 2 ply1sclf1 ⊢ ( 𝑅 ∈ Ring → 𝐴 : 𝐾 –1-1→ 𝐵 )
34 16 33 syl ⊢ ( 𝜑 → 𝐴 : 𝐾 –1-1→ 𝐵 )
35 8 1 3 2 10 11 12 fveval1fvcl ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) ∈ 𝐾 )
36 3 13 ring0cl ⊢ ( 𝑅 ∈ Ring → 0 ∈ 𝐾 )
37 16 36 syl ⊢ ( 𝜑 → 0 ∈ 𝐾 )
38 f1fveq ⊢ ( ( 𝐴 : 𝐾 –1-1→ 𝐵 ∧ ( ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) ∈ 𝐾 ∧ 0 ∈ 𝐾 ) ) → ( ( 𝐴 ‘ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) ) = ( 𝐴 ‘ 0 ) ↔ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) = 0 ) )
39 34 35 37 38 syl12anc ⊢ ( 𝜑 → ( ( 𝐴 ‘ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) ) = ( 𝐴 ‘ 0 ) ↔ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) = 0 ) )
40 27 32 39 3bitrd ⊢ ( 𝜑 → ( 𝐺 ∥ 𝐹 ↔ ( ( 𝑂 ‘ 𝐹 ) ‘ 𝑁 ) = 0 ) )