ply1rem

Description: The polynomial remainder theorem, or little Bézout's theorem (by contrast to the regular Bézout's theorem bezout ). If a polynomial F is divided by the linear factor x - A , the remainder is equal to F ( A ) , the evaluation of the polynomial at A (interpreted as a constant polynomial). (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	ply1rem.p	$⊢ P = {Poly}_{1} (R)$
	ply1rem.b	$⊢ B = {Base}_{P}$
	ply1rem.k	$⊢ K = {Base}_{R}$
	ply1rem.x	$⊢ X = {var}_{1} (R)$
	ply1rem.m	$⊢ \underset{˙}{-} = -_{P}$
	ply1rem.a	$⊢ A = algSc (P)$
	ply1rem.g	$⊢ G = X \underset{˙}{-} A (N)$
	ply1rem.o	$⊢ O = {eval}_{1} (R)$
	ply1rem.1	$⊢ φ \to R \in NzRing$
	ply1rem.2	$⊢ φ \to R \in CRing$
	ply1rem.3	$⊢ φ \to N \in K$
	ply1rem.4	$⊢ φ \to F \in B$
	ply1rem.e	$⊢ E = {rem}_{1p} (R)$
Assertion	ply1rem	$⊢ φ \to F E G = A (O (F) (N))$

Proof

Step	Hyp	Ref	Expression
1		ply1rem.p	$⊢ P = {Poly}_{1} (R)$
2		ply1rem.b	$⊢ B = {Base}_{P}$
3		ply1rem.k	$⊢ K = {Base}_{R}$
4		ply1rem.x	$⊢ X = {var}_{1} (R)$
5		ply1rem.m	$⊢ \underset{˙}{-} = -_{P}$
6		ply1rem.a	$⊢ A = algSc (P)$
7		ply1rem.g	$⊢ G = X \underset{˙}{-} A (N)$
8		ply1rem.o	$⊢ O = {eval}_{1} (R)$
9		ply1rem.1	$⊢ φ \to R \in NzRing$
10		ply1rem.2	$⊢ φ \to R \in CRing$
11		ply1rem.3	$⊢ φ \to N \in K$
12		ply1rem.4	$⊢ φ \to F \in B$
13		ply1rem.e	$⊢ E = {rem}_{1p} (R)$
14		nzrring	$⊢ R \in NzRing \to R \in Ring$
15	9 14	syl	$⊢ φ \to R \in Ring$
16		eqid	$⊢ {Monic}_{1p} (R) = {Monic}_{1p} (R)$
17		eqid	$⊢ \deg_{1} (R) = \deg_{1} (R)$
18		eqid	$⊢ 0_{R} = 0_{R}$
19	1 2 3 4 5 6 7 8 9 10 11 16 17 18	ply1remlem	$⊢ φ \to (G \in {Monic}_{1p} (R) \land \deg_{1} (R) (G) = 1 \land {O (G)}^{-1} [\{0_{R}\}] = \{N\})$
20	19	simp1d	$⊢ φ \to G \in {Monic}_{1p} (R)$
21		eqid	$⊢ {Unic}_{1p} (R) = {Unic}_{1p} (R)$
22	21 16	mon1puc1p	$⊢ (R \in Ring \land G \in {Monic}_{1p} (R)) \to G \in {Unic}_{1p} (R)$
23	15 20 22	syl2anc	$⊢ φ \to G \in {Unic}_{1p} (R)$
24	13 1 2 21 17	r1pdeglt	$⊢ (R \in Ring \land F \in B \land G \in {Unic}_{1p} (R)) \to \deg_{1} (R) (F E G) < \deg_{1} (R) (G)$
25	15 12 23 24	syl3anc	$⊢ φ \to \deg_{1} (R) (F E G) < \deg_{1} (R) (G)$
26	19	simp2d	$⊢ φ \to \deg_{1} (R) (G) = 1$
27	25 26	breqtrd	$⊢ φ \to \deg_{1} (R) (F E G) < 1$
28		1e0p1	$⊢ 1 = 0 + 1$
29	27 28	breqtrdi	$⊢ φ \to \deg_{1} (R) (F E G) < 0 + 1$
30		0nn0	$⊢ 0 \in ℕ_{0}$
31		nn0leltp1	$⊢ (\deg_{1} (R) (F E G) \in ℕ_{0} \land 0 \in ℕ_{0}) \to (\deg_{1} (R) (F E G) \leq 0 \leftrightarrow \deg_{1} (R) (F E G) < 0 + 1)$
32	30 31	mpan2	$⊢ \deg_{1} (R) (F E G) \in ℕ_{0} \to (\deg_{1} (R) (F E G) \leq 0 \leftrightarrow \deg_{1} (R) (F E G) < 0 + 1)$
33	29 32	syl5ibrcom	$⊢ φ \to (\deg_{1} (R) (F E G) \in ℕ_{0} \to \deg_{1} (R) (F E G) \leq 0)$
34		elsni	$⊢ \deg_{1} (R) (F E G) \in \{−∞\} \to \deg_{1} (R) (F E G) = −∞$
35		0xr	$⊢ 0 \in ℝ^{*}$
36		mnfle	$⊢ 0 \in ℝ^{*} \to −∞ \leq 0$
37	35 36	ax-mp	$⊢ −∞ \leq 0$
38	34 37	eqbrtrdi	$⊢ \deg_{1} (R) (F E G) \in \{−∞\} \to \deg_{1} (R) (F E G) \leq 0$
39	38	a1i	$⊢ φ \to (\deg_{1} (R) (F E G) \in \{−∞\} \to \deg_{1} (R) (F E G) \leq 0)$
40	13 1 2 21	r1pcl	$⊢ (R \in Ring \land F \in B \land G \in {Unic}_{1p} (R)) \to F E G \in B$
41	15 12 23 40	syl3anc	$⊢ φ \to F E G \in B$
42	17 1 2	deg1cl	$⊢ F E G \in B \to \deg_{1} (R) (F E G) \in (ℕ_{0} \cup \{−∞\})$
43	41 42	syl	$⊢ φ \to \deg_{1} (R) (F E G) \in (ℕ_{0} \cup \{−∞\})$
44		elun	$⊢ \deg_{1} (R) (F E G) \in (ℕ_{0} \cup \{−∞\}) \leftrightarrow (\deg_{1} (R) (F E G) \in ℕ_{0} \lor \deg_{1} (R) (F E G) \in \{−∞\})$
45	43 44	sylib	$⊢ φ \to (\deg_{1} (R) (F E G) \in ℕ_{0} \lor \deg_{1} (R) (F E G) \in \{−∞\})$
46	33 39 45	mpjaod	$⊢ φ \to \deg_{1} (R) (F E G) \leq 0$
47	17 1 2 6	deg1le0	$⊢ (R \in Ring \land F E G \in B) \to (\deg_{1} (R) (F E G) \leq 0 \leftrightarrow F E G = A ({coe}_{1} (F E G) (0)))$
48	15 41 47	syl2anc	$⊢ φ \to (\deg_{1} (R) (F E G) \leq 0 \leftrightarrow F E G = A ({coe}_{1} (F E G) (0)))$
49	46 48	mpbid	$⊢ φ \to F E G = A ({coe}_{1} (F E G) (0))$
50		eqid	$⊢ {quot}_{1p} (R) = {quot}_{1p} (R)$
51		eqid	$⊢ \cdot_{P} = \cdot_{P}$
52		eqid	$⊢ +_{P} = +_{P}$
53	1 2 21 50 13 51 52	r1pid	$⊢ (R \in Ring \land F \in B \land G \in {Unic}_{1p} (R)) \to F = ((F {quot}_{1p} (R) G) \cdot_{P} G) +_{P} (F E G)$
54	15 12 23 53	syl3anc	$⊢ φ \to F = ((F {quot}_{1p} (R) G) \cdot_{P} G) +_{P} (F E G)$
55	54	fveq2d	$⊢ φ \to O (F) = O (((F {quot}_{1p} (R) G) \cdot_{P} G) +_{P} (F E G))$
56		eqid	$⊢ R ↑_{𝑠} K = R ↑_{𝑠} K$
57	8 1 56 3	evl1rhm	$⊢ R \in CRing \to O \in (P RingHom (R ↑_{𝑠} K))$
58	10 57	syl	$⊢ φ \to O \in (P RingHom (R ↑_{𝑠} K))$
59		rhmghm	$⊢ O \in (P RingHom (R ↑_{𝑠} K)) \to O \in (P GrpHom (R ↑_{𝑠} K))$
60	58 59	syl	$⊢ φ \to O \in (P GrpHom (R ↑_{𝑠} K))$
61	1	ply1ring	$⊢ R \in Ring \to P \in Ring$
62	15 61	syl	$⊢ φ \to P \in Ring$
63	50 1 2 21	q1pcl	$⊢ (R \in Ring \land F \in B \land G \in {Unic}_{1p} (R)) \to F {quot}_{1p} (R) G \in B$
64	15 12 23 63	syl3anc	$⊢ φ \to F {quot}_{1p} (R) G \in B$
65	1 2 16	mon1pcl	$⊢ G \in {Monic}_{1p} (R) \to G \in B$
66	20 65	syl	$⊢ φ \to G \in B$
67	2 51	ringcl	$⊢ (P \in Ring \land F {quot}_{1p} (R) G \in B \land G \in B) \to (F {quot}_{1p} (R) G) \cdot_{P} G \in B$
68	62 64 66 67	syl3anc	$⊢ φ \to (F {quot}_{1p} (R) G) \cdot_{P} G \in B$
69		eqid	$⊢ +_{(R ↑_{𝑠} K)} = +_{(R ↑_{𝑠} K)}$
70	2 52 69	ghmlin	$⊢ (O \in (P GrpHom (R ↑_{𝑠} K)) \land (F {quot}_{1p} (R) G) \cdot_{P} G \in B \land F E G \in B) \to O (((F {quot}_{1p} (R) G) \cdot_{P} G) +_{P} (F E G)) = O ((F {quot}_{1p} (R) G) \cdot_{P} G) +_{(R ↑_{𝑠} K)} O (F E G)$
71	60 68 41 70	syl3anc	$⊢ φ \to O (((F {quot}_{1p} (R) G) \cdot_{P} G) +_{P} (F E G)) = O ((F {quot}_{1p} (R) G) \cdot_{P} G) +_{(R ↑_{𝑠} K)} O (F E G)$
72		eqid	$⊢ {Base}_{(R ↑_{𝑠} K)} = {Base}_{(R ↑_{𝑠} K)}$
73	3	fvexi	$⊢ K \in V$
74	73	a1i	$⊢ φ \to K \in V$
75	2 72	rhmf	$⊢ O \in (P RingHom (R ↑_{𝑠} K)) \to O : B ⟶ {Base}_{(R ↑_{𝑠} K)}$
76	58 75	syl	$⊢ φ \to O : B ⟶ {Base}_{(R ↑_{𝑠} K)}$
77	76 68	ffvelcdmd	$⊢ φ \to O ((F {quot}_{1p} (R) G) \cdot_{P} G) \in {Base}_{(R ↑_{𝑠} K)}$
78	76 41	ffvelcdmd	$⊢ φ \to O (F E G) \in {Base}_{(R ↑_{𝑠} K)}$
79		eqid	$⊢ +_{R} = +_{R}$
80	56 72 9 74 77 78 79 69	pwsplusgval	$⊢ φ \to O ((F {quot}_{1p} (R) G) \cdot_{P} G) +_{(R ↑_{𝑠} K)} O (F E G) = O ((F {quot}_{1p} (R) G) \cdot_{P} G) {+_{R}}_{f} O (F E G)$
81	55 71 80	3eqtrd	$⊢ φ \to O (F) = O ((F {quot}_{1p} (R) G) \cdot_{P} G) {+_{R}}_{f} O (F E G)$
82	81	fveq1d	$⊢ φ \to O (F) (N) = (O ((F {quot}_{1p} (R) G) \cdot_{P} G) {+_{R}}_{f} O (F E G)) (N)$
83	56 3 72 9 74 77	pwselbas	$⊢ φ \to O ((F {quot}_{1p} (R) G) \cdot_{P} G) : K ⟶ K$
84	83	ffnd	$⊢ φ \to O ((F {quot}_{1p} (R) G) \cdot_{P} G) Fn K$
85	56 3 72 9 74 78	pwselbas	$⊢ φ \to O (F E G) : K ⟶ K$
86	85	ffnd	$⊢ φ \to O (F E G) Fn K$
87		fnfvof	$⊢ ((O ((F {quot}_{1p} (R) G) \cdot_{P} G) Fn K \land O (F E G) Fn K) \land (K \in V \land N \in K)) \to (O ((F {quot}_{1p} (R) G) \cdot_{P} G) {+_{R}}_{f} O (F E G)) (N) = O ((F {quot}_{1p} (R) G) \cdot_{P} G) (N) +_{R} O (F E G) (N)$
88	84 86 74 11 87	syl22anc	$⊢ φ \to (O ((F {quot}_{1p} (R) G) \cdot_{P} G) {+_{R}}_{f} O (F E G)) (N) = O ((F {quot}_{1p} (R) G) \cdot_{P} G) (N) +_{R} O (F E G) (N)$
89		eqid	$⊢ \cdot_{(R ↑_{𝑠} K)} = \cdot_{(R ↑_{𝑠} K)}$
90	2 51 89	rhmmul	$⊢ (O \in (P RingHom (R ↑_{𝑠} K)) \land F {quot}_{1p} (R) G \in B \land G \in B) \to O ((F {quot}_{1p} (R) G) \cdot_{P} G) = O (F {quot}_{1p} (R) G) \cdot_{(R ↑_{𝑠} K)} O (G)$
91	58 64 66 90	syl3anc	$⊢ φ \to O ((F {quot}_{1p} (R) G) \cdot_{P} G) = O (F {quot}_{1p} (R) G) \cdot_{(R ↑_{𝑠} K)} O (G)$
92	76 64	ffvelcdmd	$⊢ φ \to O (F {quot}_{1p} (R) G) \in {Base}_{(R ↑_{𝑠} K)}$
93	76 66	ffvelcdmd	$⊢ φ \to O (G) \in {Base}_{(R ↑_{𝑠} K)}$
94		eqid	$⊢ \cdot_{R} = \cdot_{R}$
95	56 72 9 74 92 93 94 89	pwsmulrval	$⊢ φ \to O (F {quot}_{1p} (R) G) \cdot_{(R ↑_{𝑠} K)} O (G) = O (F {quot}_{1p} (R) G) {\cdot_{R}}_{f} O (G)$
96	91 95	eqtrd	$⊢ φ \to O ((F {quot}_{1p} (R) G) \cdot_{P} G) = O (F {quot}_{1p} (R) G) {\cdot_{R}}_{f} O (G)$
97	96	fveq1d	$⊢ φ \to O ((F {quot}_{1p} (R) G) \cdot_{P} G) (N) = (O (F {quot}_{1p} (R) G) {\cdot_{R}}_{f} O (G)) (N)$
98	56 3 72 9 74 92	pwselbas	$⊢ φ \to O (F {quot}_{1p} (R) G) : K ⟶ K$
99	98	ffnd	$⊢ φ \to O (F {quot}_{1p} (R) G) Fn K$
100	56 3 72 9 74 93	pwselbas	$⊢ φ \to O (G) : K ⟶ K$
101	100	ffnd	$⊢ φ \to O (G) Fn K$
102		fnfvof	$⊢ ((O (F {quot}_{1p} (R) G) Fn K \land O (G) Fn K) \land (K \in V \land N \in K)) \to (O (F {quot}_{1p} (R) G) {\cdot_{R}}_{f} O (G)) (N) = O (F {quot}_{1p} (R) G) (N) \cdot_{R} O (G) (N)$
103	99 101 74 11 102	syl22anc	$⊢ φ \to (O (F {quot}_{1p} (R) G) {\cdot_{R}}_{f} O (G)) (N) = O (F {quot}_{1p} (R) G) (N) \cdot_{R} O (G) (N)$
104		snidg	$⊢ N \in K \to N \in \{N\}$
105	11 104	syl	$⊢ φ \to N \in \{N\}$
106	19	simp3d	$⊢ φ \to {O (G)}^{-1} [\{0_{R}\}] = \{N\}$
107	105 106	eleqtrrd	$⊢ φ \to N \in {O (G)}^{-1} [\{0_{R}\}]$
108		fniniseg	$⊢ O (G) Fn K \to (N \in {O (G)}^{-1} [\{0_{R}\}] \leftrightarrow (N \in K \land O (G) (N) = 0_{R}))$
109	101 108	syl	$⊢ φ \to (N \in {O (G)}^{-1} [\{0_{R}\}] \leftrightarrow (N \in K \land O (G) (N) = 0_{R}))$
110	107 109	mpbid	$⊢ φ \to (N \in K \land O (G) (N) = 0_{R})$
111	110	simprd	$⊢ φ \to O (G) (N) = 0_{R}$
112	111	oveq2d	$⊢ φ \to O (F {quot}_{1p} (R) G) (N) \cdot_{R} O (G) (N) = O (F {quot}_{1p} (R) G) (N) \cdot_{R} 0_{R}$
113	98 11	ffvelcdmd	$⊢ φ \to O (F {quot}_{1p} (R) G) (N) \in K$
114	3 94 18	ringrz	$⊢ (R \in Ring \land O (F {quot}_{1p} (R) G) (N) \in K) \to O (F {quot}_{1p} (R) G) (N) \cdot_{R} 0_{R} = 0_{R}$
115	15 113 114	syl2anc	$⊢ φ \to O (F {quot}_{1p} (R) G) (N) \cdot_{R} 0_{R} = 0_{R}$
116	112 115	eqtrd	$⊢ φ \to O (F {quot}_{1p} (R) G) (N) \cdot_{R} O (G) (N) = 0_{R}$
117	97 103 116	3eqtrd	$⊢ φ \to O ((F {quot}_{1p} (R) G) \cdot_{P} G) (N) = 0_{R}$
118	117	oveq1d	$⊢ φ \to O ((F {quot}_{1p} (R) G) \cdot_{P} G) (N) +_{R} O (F E G) (N) = 0_{R} +_{R} O (F E G) (N)$
119		ringgrp	$⊢ R \in Ring \to R \in Grp$
120	15 119	syl	$⊢ φ \to R \in Grp$
121	85 11	ffvelcdmd	$⊢ φ \to O (F E G) (N) \in K$
122	3 79 18	grplid	$⊢ (R \in Grp \land O (F E G) (N) \in K) \to 0_{R} +_{R} O (F E G) (N) = O (F E G) (N)$
123	120 121 122	syl2anc	$⊢ φ \to 0_{R} +_{R} O (F E G) (N) = O (F E G) (N)$
124	88 118 123	3eqtrd	$⊢ φ \to (O ((F {quot}_{1p} (R) G) \cdot_{P} G) {+_{R}}_{f} O (F E G)) (N) = O (F E G) (N)$
125	49	fveq2d	$⊢ φ \to O (F E G) = O (A ({coe}_{1} (F E G) (0)))$
126		eqid	$⊢ {coe}_{1} (F E G) = {coe}_{1} (F E G)$
127	126 2 1 3	coe1f	$⊢ F E G \in B \to {coe}_{1} (F E G) : ℕ_{0} ⟶ K$
128	41 127	syl	$⊢ φ \to {coe}_{1} (F E G) : ℕ_{0} ⟶ K$
129		ffvelcdm	$⊢ ({coe}_{1} (F E G) : ℕ_{0} ⟶ K \land 0 \in ℕ_{0}) \to {coe}_{1} (F E G) (0) \in K$
130	128 30 129	sylancl	$⊢ φ \to {coe}_{1} (F E G) (0) \in K$
131	8 1 3 6	evl1sca	$⊢ (R \in CRing \land {coe}_{1} (F E G) (0) \in K) \to O (A ({coe}_{1} (F E G) (0))) = K \times \{{coe}_{1} (F E G) (0)\}$
132	10 130 131	syl2anc	$⊢ φ \to O (A ({coe}_{1} (F E G) (0))) = K \times \{{coe}_{1} (F E G) (0)\}$
133	125 132	eqtrd	$⊢ φ \to O (F E G) = K \times \{{coe}_{1} (F E G) (0)\}$
134	133	fveq1d	$⊢ φ \to O (F E G) (N) = (K \times \{{coe}_{1} (F E G) (0)\}) (N)$
135		fvex	$⊢ {coe}_{1} (F E G) (0) \in V$
136	135	fvconst2	$⊢ N \in K \to (K \times \{{coe}_{1} (F E G) (0)\}) (N) = {coe}_{1} (F E G) (0)$
137	11 136	syl	$⊢ φ \to (K \times \{{coe}_{1} (F E G) (0)\}) (N) = {coe}_{1} (F E G) (0)$
138	134 137	eqtrd	$⊢ φ \to O (F E G) (N) = {coe}_{1} (F E G) (0)$
139	82 124 138	3eqtrd	$⊢ φ \to O (F) (N) = {coe}_{1} (F E G) (0)$
140	139	fveq2d	$⊢ φ \to A (O (F) (N)) = A ({coe}_{1} (F E G) (0))$
141	49 140	eqtr4d	$⊢ φ \to F E G = A (O (F) (N))$

Metamath Proof Explorer

Theorem ply1rem

Proof