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