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	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	ply1rem.b	$$⊢B={\mathrm{Base}}_P$$
	ply1rem.k	$$⊢K={\mathrm{Base}}_R$$
	ply1rem.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
	ply1rem.m	$$⊢\underset{\dot{}}{-}={-}_P$$
	ply1rem.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
	ply1rem.g	$$⊢G=X\underset{\dot{}}{-}A\left(N\right)$$
	ply1rem.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
	ply1rem.1	$$⊢\phi \to R\in \mathrm{NzRing}$$
	ply1rem.2	$$⊢\phi \to R\in \mathrm{CRing}$$
	ply1rem.3	$$⊢\phi \to N\in K$$
	ply1rem.4	$$⊢\phi \to F\in B$$
	facth1.z	$$⊢\underset{\dot{}}{0}=0_R$$
	facth1.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(P\right)$$
Assertion	facth1	$$⊢\phi \to \left(G\underset{\dot{}}{\parallel }F\leftrightarrow O\left(F\right)\left(N\right)=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ply1rem.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		ply1rem.b	$$⊢B={\mathrm{Base}}_P$$
3		ply1rem.k	$$⊢K={\mathrm{Base}}_R$$
4		ply1rem.x	$$⊢X={\mathrm{var}}_1\left(R\right)$$
5		ply1rem.m	$$⊢\underset{\dot{}}{-}={-}_P$$
6		ply1rem.a	$$⊢A=\mathrm{algSc}\left(P\right)$$
7		ply1rem.g	$$⊢G=X\underset{\dot{}}{-}A\left(N\right)$$
8		ply1rem.o	$$⊢O={\mathrm{eval}}_1\left(R\right)$$
9		ply1rem.1	$$⊢\phi \to R\in \mathrm{NzRing}$$
10		ply1rem.2	$$⊢\phi \to R\in \mathrm{CRing}$$
11		ply1rem.3	$$⊢\phi \to N\in K$$
12		ply1rem.4	$$⊢\phi \to F\in B$$
13		facth1.z	$$⊢\underset{\dot{}}{0}=0_R$$
14		facth1.d	$$⊢\underset{\dot{}}{\parallel }={\parallel }_r\left(P\right)$$
15		nzrring	$$⊢R\in \mathrm{NzRing}\to R\in \mathrm{Ring}$$
16	9 15	syl	$$⊢\phi \to R\in \mathrm{Ring}$$
17		eqid	$$⊢{Monic}_{\mathrm{1p}}\left(R\right)={Monic}_{\mathrm{1p}}\left(R\right)$$
18		eqid	$$⊢{\mathrm{deg}}_1\left(R\right)={\mathrm{deg}}_1\left(R\right)$$
19	1 2 3 4 5 6 7 8 9 10 11 17 18 13	ply1remlem	$$⊢\phi \to \left(G\in {Monic}_{\mathrm{1p}}\left(R\right)\wedge {\mathrm{deg}}_1\left(R\right)\left(G\right)=1\wedge {O\left(G\right)}^{-1}\left[\left\{\underset{\dot{}}{0}\right\}\right]=\left\{N\right\}\right)$$
20	19	simp1d	$$⊢\phi \to G\in {Monic}_{\mathrm{1p}}\left(R\right)$$
21		eqid	$$⊢{Unic}_{\mathrm{1p}}\left(R\right)={Unic}_{\mathrm{1p}}\left(R\right)$$
22	21 17	mon1puc1p	$$⊢\left(R\in \mathrm{Ring}\wedge G\in {Monic}_{\mathrm{1p}}\left(R\right)\right)\to G\in {Unic}_{\mathrm{1p}}\left(R\right)$$
23	16 20 22	syl2anc	$$⊢\phi \to G\in {Unic}_{\mathrm{1p}}\left(R\right)$$
24		eqid	$$⊢0_P=0_P$$
25		eqid	$$⊢{rem}_{\mathrm{1p}}\left(R\right)={rem}_{\mathrm{1p}}\left(R\right)$$
26	1 14 2 21 24 25	dvdsr1p	$$⊢\left(R\in \mathrm{Ring}\wedge F\in B\wedge G\in {Unic}_{\mathrm{1p}}\left(R\right)\right)\to \left(G\underset{\dot{}}{\parallel }F\leftrightarrow F{rem}_{\mathrm{1p}}\left(R\right)G=0_P\right)$$
27	16 12 23 26	syl3anc	$$⊢\phi \to \left(G\underset{\dot{}}{\parallel }F\leftrightarrow F{rem}_{\mathrm{1p}}\left(R\right)G=0_P\right)$$
28	1 2 3 4 5 6 7 8 9 10 11 12 25	ply1rem	$$⊢\phi \to F{rem}_{\mathrm{1p}}\left(R\right)G=A\left(O\left(F\right)\left(N\right)\right)$$
29	1 6 13 24	ply1scl0	$$⊢R\in \mathrm{Ring}\to A\left(\underset{\dot{}}{0}\right)=0_P$$
30	16 29	syl	$$⊢\phi \to A\left(\underset{\dot{}}{0}\right)=0_P$$
31	30	eqcomd	$$⊢\phi \to 0_P=A\left(\underset{\dot{}}{0}\right)$$
32	28 31	eqeq12d	$$⊢\phi \to \left(F{rem}_{\mathrm{1p}}\left(R\right)G=0_P\leftrightarrow A\left(O\left(F\right)\left(N\right)\right)=A\left(\underset{\dot{}}{0}\right)\right)$$
33	1 6 3 2	ply1sclf1	$$⊢R\in \mathrm{Ring}\to A:K\underset{1-1}{⟶}B$$
34	16 33	syl	$$⊢\phi \to A:K\underset{1-1}{⟶}B$$
35	8 1 3 2 10 11 12	fveval1fvcl	$$⊢\phi \to O\left(F\right)\left(N\right)\in K$$
36	3 13	ring0cl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{0}\in K$$
37	16 36	syl	$$⊢\phi \to \underset{\dot{}}{0}\in K$$
38		f1fveq	$$⊢\left(A:K\underset{1-1}{⟶}B\wedge \left(O\left(F\right)\left(N\right)\in K\wedge \underset{\dot{}}{0}\in K\right)\right)\to \left(A\left(O\left(F\right)\left(N\right)\right)=A\left(\underset{\dot{}}{0}\right)\leftrightarrow O\left(F\right)\left(N\right)=\underset{\dot{}}{0}\right)$$
39	34 35 37 38	syl12anc	$$⊢\phi \to \left(A\left(O\left(F\right)\left(N\right)\right)=A\left(\underset{\dot{}}{0}\right)\leftrightarrow O\left(F\right)\left(N\right)=\underset{\dot{}}{0}\right)$$
40	27 32 39	3bitrd	$$⊢\phi \to \left(G\underset{\dot{}}{\parallel }F\leftrightarrow O\left(F\right)\left(N\right)=\underset{\dot{}}{0}\right)$$