plydiveu

	Ref	Expression
Hypotheses	plydiv.pl	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
	plydiv.tm	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
	plydiv.rc	$⊢ (φ \land (x \in S \land x \neq 0)) \to \frac{1}{x} \in S$
	plydiv.m1	$⊢ φ \to - 1 \in S$
	plydiv.f	$⊢ φ \to F \in Poly (S)$
	plydiv.g	$⊢ φ \to G \in Poly (S)$
	plydiv.z	$⊢ φ \to G \neq 0_{𝑝}$
	plydiv.r	$⊢ R = F -_{f} (G \times_{f} q)$
	plydiveu.q	$⊢ φ \to q \in Poly (S)$
	plydiveu.qd	$⊢ φ \to (R = 0_{𝑝} \lor \deg (R) < \deg (G))$
	plydiveu.t	$⊢ T = F -_{f} (G \times_{f} p)$
	plydiveu.p	$⊢ φ \to p \in Poly (S)$
	plydiveu.pd	$⊢ φ \to (T = 0_{𝑝} \lor \deg (T) < \deg (G))$
Assertion	plydiveu	$⊢ φ \to p = q$

Proof

Step	Hyp	Ref	Expression
1		plydiv.pl	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
2		plydiv.tm	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
3		plydiv.rc	$⊢ (φ \land (x \in S \land x \neq 0)) \to \frac{1}{x} \in S$
4		plydiv.m1	$⊢ φ \to - 1 \in S$
5		plydiv.f	$⊢ φ \to F \in Poly (S)$
6		plydiv.g	$⊢ φ \to G \in Poly (S)$
7		plydiv.z	$⊢ φ \to G \neq 0_{𝑝}$
8		plydiv.r	$⊢ R = F -_{f} (G \times_{f} q)$
9		plydiveu.q	$⊢ φ \to q \in Poly (S)$
10		plydiveu.qd	$⊢ φ \to (R = 0_{𝑝} \lor \deg (R) < \deg (G))$
11		plydiveu.t	$⊢ T = F -_{f} (G \times_{f} p)$
12		plydiveu.p	$⊢ φ \to p \in Poly (S)$
13		plydiveu.pd	$⊢ φ \to (T = 0_{𝑝} \lor \deg (T) < \deg (G))$
14		idd	$⊢ φ \to (p -_{f} q = 0_{𝑝} \to p -_{f} q = 0_{𝑝})$
15	1 2 3 4 5 6 7 8	plydivlem2	$⊢ (φ \land q \in Poly (S)) \to R \in Poly (S)$
16	9 15	mpdan	$⊢ φ \to R \in Poly (S)$
17	1 2 3 4 5 6 7 11	plydivlem2	$⊢ (φ \land p \in Poly (S)) \to T \in Poly (S)$
18	12 17	mpdan	$⊢ φ \to T \in Poly (S)$
19	16 18 1 2 4	plysub	$⊢ φ \to R -_{f} T \in Poly (S)$
20		dgrcl	$⊢ R -_{f} T \in Poly (S) \to \deg (R -_{f} T) \in ℕ_{0}$
21	19 20	syl	$⊢ φ \to \deg (R -_{f} T) \in ℕ_{0}$
22	21	nn0red	$⊢ φ \to \deg (R -_{f} T) \in ℝ$
23		dgrcl	$⊢ T \in Poly (S) \to \deg (T) \in ℕ_{0}$
24	18 23	syl	$⊢ φ \to \deg (T) \in ℕ_{0}$
25	24	nn0red	$⊢ φ \to \deg (T) \in ℝ$
26		dgrcl	$⊢ R \in Poly (S) \to \deg (R) \in ℕ_{0}$
27	16 26	syl	$⊢ φ \to \deg (R) \in ℕ_{0}$
28	27	nn0red	$⊢ φ \to \deg (R) \in ℝ$
29	25 28	ifcld	$⊢ φ \to if (\deg (R) \leq \deg (T), \deg (T), \deg (R)) \in ℝ$
30		dgrcl	$⊢ G \in Poly (S) \to \deg (G) \in ℕ_{0}$
31	6 30	syl	$⊢ φ \to \deg (G) \in ℕ_{0}$
32	31	nn0red	$⊢ φ \to \deg (G) \in ℝ$
33		eqid	$⊢ \deg (R) = \deg (R)$
34		eqid	$⊢ \deg (T) = \deg (T)$
35	33 34	dgrsub	$⊢ (R \in Poly (S) \land T \in Poly (S)) \to \deg (R -_{f} T) \leq if (\deg (R) \leq \deg (T), \deg (T), \deg (R))$
36	16 18 35	syl2anc	$⊢ φ \to \deg (R -_{f} T) \leq if (\deg (R) \leq \deg (T), \deg (T), \deg (R))$
37		eqid	$⊢ coeff (T) = coeff (T)$
38	34 37	dgrlt	$⊢ (T \in Poly (S) \land \deg (G) \in ℕ_{0}) \to ((T = 0_{𝑝} \lor \deg (T) < \deg (G)) \leftrightarrow (\deg (T) \leq \deg (G) \land coeff (T) (\deg (G)) = 0))$
39	18 31 38	syl2anc	$⊢ φ \to ((T = 0_{𝑝} \lor \deg (T) < \deg (G)) \leftrightarrow (\deg (T) \leq \deg (G) \land coeff (T) (\deg (G)) = 0))$
40	13 39	mpbid	$⊢ φ \to (\deg (T) \leq \deg (G) \land coeff (T) (\deg (G)) = 0)$
41	40	simpld	$⊢ φ \to \deg (T) \leq \deg (G)$
42		eqid	$⊢ coeff (R) = coeff (R)$
43	33 42	dgrlt	$⊢ (R \in Poly (S) \land \deg (G) \in ℕ_{0}) \to ((R = 0_{𝑝} \lor \deg (R) < \deg (G)) \leftrightarrow (\deg (R) \leq \deg (G) \land coeff (R) (\deg (G)) = 0))$
44	16 31 43	syl2anc	$⊢ φ \to ((R = 0_{𝑝} \lor \deg (R) < \deg (G)) \leftrightarrow (\deg (R) \leq \deg (G) \land coeff (R) (\deg (G)) = 0))$
45	10 44	mpbid	$⊢ φ \to (\deg (R) \leq \deg (G) \land coeff (R) (\deg (G)) = 0)$
46	45	simpld	$⊢ φ \to \deg (R) \leq \deg (G)$
47		breq1	$⊢ \deg (T) = if (\deg (R) \leq \deg (T), \deg (T), \deg (R)) \to (\deg (T) \leq \deg (G) \leftrightarrow if (\deg (R) \leq \deg (T), \deg (T), \deg (R)) \leq \deg (G))$
48		breq1	$⊢ \deg (R) = if (\deg (R) \leq \deg (T), \deg (T), \deg (R)) \to (\deg (R) \leq \deg (G) \leftrightarrow if (\deg (R) \leq \deg (T), \deg (T), \deg (R)) \leq \deg (G))$
49	47 48	ifboth	$⊢ (\deg (T) \leq \deg (G) \land \deg (R) \leq \deg (G)) \to if (\deg (R) \leq \deg (T), \deg (T), \deg (R)) \leq \deg (G)$
50	41 46 49	syl2anc	$⊢ φ \to if (\deg (R) \leq \deg (T), \deg (T), \deg (R)) \leq \deg (G)$
51	22 29 32 36 50	letrd	$⊢ φ \to \deg (R -_{f} T) \leq \deg (G)$
52	51	adantr	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to \deg (R -_{f} T) \leq \deg (G)$
53	12 9 1 2 4	plysub	$⊢ φ \to p -_{f} q \in Poly (S)$
54		dgrcl	$⊢ p -_{f} q \in Poly (S) \to \deg (p -_{f} q) \in ℕ_{0}$
55	53 54	syl	$⊢ φ \to \deg (p -_{f} q) \in ℕ_{0}$
56		nn0addge1	$⊢ (\deg (G) \in ℝ \land \deg (p -_{f} q) \in ℕ_{0}) \to \deg (G) \leq \deg (G) + \deg (p -_{f} q)$
57	32 55 56	syl2anc	$⊢ φ \to \deg (G) \leq \deg (G) + \deg (p -_{f} q)$
58	57	adantr	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to \deg (G) \leq \deg (G) + \deg (p -_{f} q)$
59		plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$
60	5 59	syl	$⊢ φ \to F : ℂ ⟶ ℂ$
61	60	ffvelcdmda	$⊢ (φ \land z \in ℂ) \to F (z) \in ℂ$
62	6 9 1 2	plymul	$⊢ φ \to G \times_{f} q \in Poly (S)$
63		plyf	$⊢ G \times_{f} q \in Poly (S) \to (G \times_{f} q) : ℂ ⟶ ℂ$
64	62 63	syl	$⊢ φ \to (G \times_{f} q) : ℂ ⟶ ℂ$
65	64	ffvelcdmda	$⊢ (φ \land z \in ℂ) \to (G \times_{f} q) (z) \in ℂ$
66	6 12 1 2	plymul	$⊢ φ \to G \times_{f} p \in Poly (S)$
67		plyf	$⊢ G \times_{f} p \in Poly (S) \to (G \times_{f} p) : ℂ ⟶ ℂ$
68	66 67	syl	$⊢ φ \to (G \times_{f} p) : ℂ ⟶ ℂ$
69	68	ffvelcdmda	$⊢ (φ \land z \in ℂ) \to (G \times_{f} p) (z) \in ℂ$
70	61 65 69	nnncan1d	$⊢ (φ \land z \in ℂ) \to F (z) - (G \times_{f} q) (z) - (F (z) - (G \times_{f} p) (z)) = (G \times_{f} p) (z) - (G \times_{f} q) (z)$
71	70	mpteq2dva	$⊢ φ \to (z \in ℂ ⟼ F (z) - (G \times_{f} q) (z) - (F (z) - (G \times_{f} p) (z))) = (z \in ℂ ⟼ (G \times_{f} p) (z) - (G \times_{f} q) (z))$
72		cnex	$⊢ ℂ \in V$
73	72	a1i	$⊢ φ \to ℂ \in V$
74	61 65	subcld	$⊢ (φ \land z \in ℂ) \to F (z) - (G \times_{f} q) (z) \in ℂ$
75	61 69	subcld	$⊢ (φ \land z \in ℂ) \to F (z) - (G \times_{f} p) (z) \in ℂ$
76	60	feqmptd	$⊢ φ \to F = (z \in ℂ ⟼ F (z))$
77	64	feqmptd	$⊢ φ \to G \times_{f} q = (z \in ℂ ⟼ (G \times_{f} q) (z))$
78	73 61 65 76 77	offval2	$⊢ φ \to F -_{f} (G \times_{f} q) = (z \in ℂ ⟼ F (z) - (G \times_{f} q) (z))$
79	8 78	eqtrid	$⊢ φ \to R = (z \in ℂ ⟼ F (z) - (G \times_{f} q) (z))$
80	68	feqmptd	$⊢ φ \to G \times_{f} p = (z \in ℂ ⟼ (G \times_{f} p) (z))$
81	73 61 69 76 80	offval2	$⊢ φ \to F -_{f} (G \times_{f} p) = (z \in ℂ ⟼ F (z) - (G \times_{f} p) (z))$
82	11 81	eqtrid	$⊢ φ \to T = (z \in ℂ ⟼ F (z) - (G \times_{f} p) (z))$
83	73 74 75 79 82	offval2	$⊢ φ \to R -_{f} T = (z \in ℂ ⟼ F (z) - (G \times_{f} q) (z) - (F (z) - (G \times_{f} p) (z)))$
84	73 69 65 80 77	offval2	$⊢ φ \to (G \times_{f} p) -_{f} (G \times_{f} q) = (z \in ℂ ⟼ (G \times_{f} p) (z) - (G \times_{f} q) (z))$
85	71 83 84	3eqtr4d	$⊢ φ \to R -_{f} T = (G \times_{f} p) -_{f} (G \times_{f} q)$
86		plyf	$⊢ G \in Poly (S) \to G : ℂ ⟶ ℂ$
87	6 86	syl	$⊢ φ \to G : ℂ ⟶ ℂ$
88		plyf	$⊢ p \in Poly (S) \to p : ℂ ⟶ ℂ$
89	12 88	syl	$⊢ φ \to p : ℂ ⟶ ℂ$
90		plyf	$⊢ q \in Poly (S) \to q : ℂ ⟶ ℂ$
91	9 90	syl	$⊢ φ \to q : ℂ ⟶ ℂ$
92		subdi	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x (y - z) = x y - x z$
93	92	adantl	$⊢ (φ \land (x \in ℂ \land y \in ℂ \land z \in ℂ)) \to x (y - z) = x y - x z$
94	73 87 89 91 93	caofdi	$⊢ φ \to G \times_{f} (p -_{f} q) = (G \times_{f} p) -_{f} (G \times_{f} q)$
95	85 94	eqtr4d	$⊢ φ \to R -_{f} T = G \times_{f} (p -_{f} q)$
96	95	fveq2d	$⊢ φ \to \deg (R -_{f} T) = \deg (G \times_{f} (p -_{f} q))$
97	96	adantr	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to \deg (R -_{f} T) = \deg (G \times_{f} (p -_{f} q))$
98	6	adantr	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to G \in Poly (S)$
99	7	adantr	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to G \neq 0_{𝑝}$
100	53	adantr	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to p -_{f} q \in Poly (S)$
101		simpr	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to p -_{f} q \neq 0_{𝑝}$
102		eqid	$⊢ \deg (G) = \deg (G)$
103		eqid	$⊢ \deg (p -_{f} q) = \deg (p -_{f} q)$
104	102 103	dgrmul	$⊢ ((G \in Poly (S) \land G \neq 0_{𝑝}) \land (p -_{f} q \in Poly (S) \land p -_{f} q \neq 0_{𝑝})) \to \deg (G \times_{f} (p -_{f} q)) = \deg (G) + \deg (p -_{f} q)$
105	98 99 100 101 104	syl22anc	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to \deg (G \times_{f} (p -_{f} q)) = \deg (G) + \deg (p -_{f} q)$
106	97 105	eqtrd	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to \deg (R -_{f} T) = \deg (G) + \deg (p -_{f} q)$
107	58 106	breqtrrd	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to \deg (G) \leq \deg (R -_{f} T)$
108	22 32	letri3d	$⊢ φ \to (\deg (R -_{f} T) = \deg (G) \leftrightarrow (\deg (R -_{f} T) \leq \deg (G) \land \deg (G) \leq \deg (R -_{f} T)))$
109	108	adantr	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to (\deg (R -_{f} T) = \deg (G) \leftrightarrow (\deg (R -_{f} T) \leq \deg (G) \land \deg (G) \leq \deg (R -_{f} T)))$
110	52 107 109	mpbir2and	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to \deg (R -_{f} T) = \deg (G)$
111	110	fveq2d	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to coeff (R -_{f} T) (\deg (R -_{f} T)) = coeff (R -_{f} T) (\deg (G))$
112	42 37	coesub	$⊢ (R \in Poly (S) \land T \in Poly (S)) \to coeff (R -_{f} T) = coeff (R) -_{f} coeff (T)$
113	16 18 112	syl2anc	$⊢ φ \to coeff (R -_{f} T) = coeff (R) -_{f} coeff (T)$
114	113	fveq1d	$⊢ φ \to coeff (R -_{f} T) (\deg (G)) = (coeff (R) -_{f} coeff (T)) (\deg (G))$
115	42	coef3	$⊢ R \in Poly (S) \to coeff (R) : ℕ_{0} ⟶ ℂ$
116		ffn	$⊢ coeff (R) : ℕ_{0} ⟶ ℂ \to coeff (R) Fn ℕ_{0}$
117	16 115 116	3syl	$⊢ φ \to coeff (R) Fn ℕ_{0}$
118	37	coef3	$⊢ T \in Poly (S) \to coeff (T) : ℕ_{0} ⟶ ℂ$
119		ffn	$⊢ coeff (T) : ℕ_{0} ⟶ ℂ \to coeff (T) Fn ℕ_{0}$
120	18 118 119	3syl	$⊢ φ \to coeff (T) Fn ℕ_{0}$
121		nn0ex	$⊢ ℕ_{0} \in V$
122	121	a1i	$⊢ φ \to ℕ_{0} \in V$
123		inidm	$⊢ ℕ_{0} \cap ℕ_{0} = ℕ_{0}$
124	45	simprd	$⊢ φ \to coeff (R) (\deg (G)) = 0$
125	124	adantr	$⊢ (φ \land \deg (G) \in ℕ_{0}) \to coeff (R) (\deg (G)) = 0$
126	40	simprd	$⊢ φ \to coeff (T) (\deg (G)) = 0$
127	126	adantr	$⊢ (φ \land \deg (G) \in ℕ_{0}) \to coeff (T) (\deg (G)) = 0$
128	117 120 122 122 123 125 127	ofval	$⊢ (φ \land \deg (G) \in ℕ_{0}) \to (coeff (R) -_{f} coeff (T)) (\deg (G)) = 0 - 0$
129	31 128	mpdan	$⊢ φ \to (coeff (R) -_{f} coeff (T)) (\deg (G)) = 0 - 0$
130	114 129	eqtrd	$⊢ φ \to coeff (R -_{f} T) (\deg (G)) = 0 - 0$
131		0m0e0	$⊢ 0 - 0 = 0$
132	130 131	eqtrdi	$⊢ φ \to coeff (R -_{f} T) (\deg (G)) = 0$
133	132	adantr	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to coeff (R -_{f} T) (\deg (G)) = 0$
134	111 133	eqtrd	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to coeff (R -_{f} T) (\deg (R -_{f} T)) = 0$
135		eqid	$⊢ \deg (R -_{f} T) = \deg (R -_{f} T)$
136		eqid	$⊢ coeff (R -_{f} T) = coeff (R -_{f} T)$
137	135 136	dgreq0	$⊢ R -_{f} T \in Poly (S) \to (R -_{f} T = 0_{𝑝} \leftrightarrow coeff (R -_{f} T) (\deg (R -_{f} T)) = 0)$
138	19 137	syl	$⊢ φ \to (R -_{f} T = 0_{𝑝} \leftrightarrow coeff (R -_{f} T) (\deg (R -_{f} T)) = 0)$
139	138	biimpar	$⊢ (φ \land coeff (R -_{f} T) (\deg (R -_{f} T)) = 0) \to R -_{f} T = 0_{𝑝}$
140	134 139	syldan	$⊢ (φ \land p -_{f} q \neq 0_{𝑝}) \to R -_{f} T = 0_{𝑝}$
141	140	ex	$⊢ φ \to (p -_{f} q \neq 0_{𝑝} \to R -_{f} T = 0_{𝑝})$
142		plymul0or	$⊢ (G \in Poly (S) \land p -_{f} q \in Poly (S)) \to (G \times_{f} (p -_{f} q) = 0_{𝑝} \leftrightarrow (G = 0_{𝑝} \lor p -_{f} q = 0_{𝑝}))$
143	6 53 142	syl2anc	$⊢ φ \to (G \times_{f} (p -_{f} q) = 0_{𝑝} \leftrightarrow (G = 0_{𝑝} \lor p -_{f} q = 0_{𝑝}))$
144	95	eqeq1d	$⊢ φ \to (R -_{f} T = 0_{𝑝} \leftrightarrow G \times_{f} (p -_{f} q) = 0_{𝑝})$
145	7	neneqd	$⊢ φ \to \neg G = 0_{𝑝}$
146		biorf	$⊢ \neg G = 0_{𝑝} \to (p -_{f} q = 0_{𝑝} \leftrightarrow (G = 0_{𝑝} \lor p -_{f} q = 0_{𝑝}))$
147	145 146	syl	$⊢ φ \to (p -_{f} q = 0_{𝑝} \leftrightarrow (G = 0_{𝑝} \lor p -_{f} q = 0_{𝑝}))$
148	143 144 147	3bitr4d	$⊢ φ \to (R -_{f} T = 0_{𝑝} \leftrightarrow p -_{f} q = 0_{𝑝})$
149	141 148	sylibd	$⊢ φ \to (p -_{f} q \neq 0_{𝑝} \to p -_{f} q = 0_{𝑝})$
150	14 149	pm2.61dne	$⊢ φ \to p -_{f} q = 0_{𝑝}$
151		df-0p	$⊢ 0_{𝑝} = ℂ \times \{0\}$
152	150 151	eqtrdi	$⊢ φ \to p -_{f} q = ℂ \times \{0\}$
153		ofsubeq0	$⊢ (ℂ \in V \land p : ℂ ⟶ ℂ \land q : ℂ ⟶ ℂ) \to (p -_{f} q = ℂ \times \{0\} \leftrightarrow p = q)$
154	72 89 91 153	mp3an2i	$⊢ φ \to (p -_{f} q = ℂ \times \{0\} \leftrightarrow p = q)$
155	152 154	mpbid	$⊢ φ \to p = q$

Metamath Proof Explorer

Theorem plydiveu

Proof