Theorem quotcan

Description: Exact division with a multiple. (Contributed by Mario Carneiro, 26-Jul-2014)

	Ref	Expression
Hypothesis	quotcan.1	⊢ 𝐻 = ( 𝐹 ∘f · 𝐺 )
Assertion	quotcan	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐻 quot 𝐺 ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		quotcan.1	⊢ 𝐻 = ( 𝐹 ∘f · 𝐺 )
2		plyssc	⊢ ( Poly ‘ 𝑆 ) ⊆ ( Poly ‘ ℂ )
3		simp2	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
4	2 3	sselid	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → 𝐺 ∈ ( Poly ‘ ℂ ) )
5		simp1	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
6	2 5	sselid	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → 𝐹 ∈ ( Poly ‘ ℂ ) )
7		plymulcl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → ( 𝐹 ∘f · 𝐺 ) ∈ ( Poly ‘ ℂ ) )
8	1 7	eqeltrid	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ) → 𝐻 ∈ ( Poly ‘ ℂ ) )
9	8	3adant3	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → 𝐻 ∈ ( Poly ‘ ℂ ) )
10		simp3	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → 𝐺 ≠ 0𝑝 )
11		quotcl2	⊢ ( ( 𝐻 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐻 quot 𝐺 ) ∈ ( Poly ‘ ℂ ) )
12	9 4 10 11	syl3anc	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐻 quot 𝐺 ) ∈ ( Poly ‘ ℂ ) )
13		plysubcl	⊢ ( ( 𝐹 ∈ ( Poly ‘ ℂ ) ∧ ( 𝐻 quot 𝐺 ) ∈ ( Poly ‘ ℂ ) ) → ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) )
14	6 12 13	syl2anc	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) )
15		plymul0or	⊢ ( ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) ) → ( ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) = 0𝑝 ↔ ( 𝐺 = 0𝑝 ∨ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = 0𝑝 ) ) )
16	4 14 15	syl2anc	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) = 0𝑝 ↔ ( 𝐺 = 0𝑝 ∨ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = 0𝑝 ) ) )
17		cnex	⊢ ℂ ∈ V
18	17	a1i	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ℂ ∈ V )
19		plyf	⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝐹 : ℂ ⟶ ℂ )
20	5 19	syl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → 𝐹 : ℂ ⟶ ℂ )
21		plyf	⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → 𝐺 : ℂ ⟶ ℂ )
22	3 21	syl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → 𝐺 : ℂ ⟶ ℂ )
23		mulcom	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
24	23	adantl	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
25	18 20 22 24	caofcom	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 ∘f · 𝐺 ) = ( 𝐺 ∘f · 𝐹 ) )
26	1 25	eqtrid	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → 𝐻 = ( 𝐺 ∘f · 𝐹 ) )
27	26	oveq1d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) = ( ( 𝐺 ∘f · 𝐹 ) ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) )
28		plyf	⊢ ( ( 𝐻 quot 𝐺 ) ∈ ( Poly ‘ ℂ ) → ( 𝐻 quot 𝐺 ) : ℂ ⟶ ℂ )
29	12 28	syl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐻 quot 𝐺 ) : ℂ ⟶ ℂ )
30		subdi	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 · ( 𝑦 − 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) − ( 𝑥 · 𝑧 ) ) )
31	30	adantl	⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( 𝑥 · ( 𝑦 − 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) − ( 𝑥 · 𝑧 ) ) )
32	18 22 20 29 31	caofdi	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) = ( ( 𝐺 ∘f · 𝐹 ) ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) )
33	27 32	eqtr4d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) = ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) )
34	33	eqeq1d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) = 0𝑝 ↔ ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) = 0𝑝 ) )
35	10	neneqd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ¬ 𝐺 = 0𝑝 )
36		biorf	⊢ ( ¬ 𝐺 = 0𝑝 → ( ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = 0𝑝 ↔ ( 𝐺 = 0𝑝 ∨ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = 0𝑝 ) ) )
37	35 36	syl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = 0𝑝 ↔ ( 𝐺 = 0𝑝 ∨ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = 0𝑝 ) ) )
38	16 34 37	3bitr4d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) = 0𝑝 ↔ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = 0𝑝 ) )
39	38	biimpd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) = 0𝑝 → ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = 0𝑝 ) )
40		eqid	⊢ ( deg ‘ 𝐺 ) = ( deg ‘ 𝐺 )
41		eqid	⊢ ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) = ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) )
42	40 41	dgrmul	⊢ ( ( ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) ∧ ( ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) ∧ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ≠ 0𝑝 ) ) → ( deg ‘ ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) = ( ( deg ‘ 𝐺 ) + ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) )
43	42	expr	⊢ ( ( ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) ∧ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) ) → ( ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ≠ 0𝑝 → ( deg ‘ ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) = ( ( deg ‘ 𝐺 ) + ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) ) )
44	4 10 14 43	syl21anc	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ≠ 0𝑝 → ( deg ‘ ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) = ( ( deg ‘ 𝐺 ) + ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) ) )
45		dgrcl	⊢ ( 𝐺 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
46	3 45	syl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( deg ‘ 𝐺 ) ∈ ℕ0 )
47	46	nn0red	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( deg ‘ 𝐺 ) ∈ ℝ )
48		dgrcl	⊢ ( ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ∈ ℕ0 )
49	14 48	syl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ∈ ℕ0 )
50		nn0addge1	⊢ ( ( ( deg ‘ 𝐺 ) ∈ ℝ ∧ ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ∈ ℕ0 ) → ( deg ‘ 𝐺 ) ≤ ( ( deg ‘ 𝐺 ) + ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) )
51	47 49 50	syl2anc	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( deg ‘ 𝐺 ) ≤ ( ( deg ‘ 𝐺 ) + ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) )
52		breq2	⊢ ( ( deg ‘ ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) = ( ( deg ‘ 𝐺 ) + ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) → ( ( deg ‘ 𝐺 ) ≤ ( deg ‘ ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) ↔ ( deg ‘ 𝐺 ) ≤ ( ( deg ‘ 𝐺 ) + ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) ) )
53	51 52	syl5ibrcom	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( deg ‘ ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) = ( ( deg ‘ 𝐺 ) + ( deg ‘ ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) → ( deg ‘ 𝐺 ) ≤ ( deg ‘ ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) ) )
54	44 53	syld	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ≠ 0𝑝 → ( deg ‘ 𝐺 ) ≤ ( deg ‘ ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) ) )
55	33	fveq2d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( deg ‘ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ) = ( deg ‘ ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) )
56	55	breq2d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( deg ‘ 𝐺 ) ≤ ( deg ‘ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ) ↔ ( deg ‘ 𝐺 ) ≤ ( deg ‘ ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) ) )
57		plymulcl	⊢ ( ( 𝐺 ∈ ( Poly ‘ ℂ ) ∧ ( 𝐻 quot 𝐺 ) ∈ ( Poly ‘ ℂ ) ) → ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) )
58	4 12 57	syl2anc	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) )
59		plysubcl	⊢ ( ( 𝐻 ∈ ( Poly ‘ ℂ ) ∧ ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ∈ ( Poly ‘ ℂ ) ) → ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ∈ ( Poly ‘ ℂ ) )
60	9 58 59	syl2anc	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ∈ ( Poly ‘ ℂ ) )
61		dgrcl	⊢ ( ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ∈ ( Poly ‘ ℂ ) → ( deg ‘ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ) ∈ ℕ0 )
62	60 61	syl	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( deg ‘ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ) ∈ ℕ0 )
63	62	nn0red	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( deg ‘ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ) ∈ ℝ )
64	47 63	lenltd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( deg ‘ 𝐺 ) ≤ ( deg ‘ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ) ↔ ¬ ( deg ‘ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ) < ( deg ‘ 𝐺 ) ) )
65	56 64	bitr3d	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( deg ‘ 𝐺 ) ≤ ( deg ‘ ( 𝐺 ∘f · ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ) ) ↔ ¬ ( deg ‘ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ) < ( deg ‘ 𝐺 ) ) )
66	54 65	sylibd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) ≠ 0𝑝 → ¬ ( deg ‘ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ) < ( deg ‘ 𝐺 ) ) )
67	66	necon4ad	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( deg ‘ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ) < ( deg ‘ 𝐺 ) → ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = 0𝑝 ) )
68		eqid	⊢ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) = ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) )
69	68	quotdgr	⊢ ( ( 𝐻 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ∈ ( Poly ‘ ℂ ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ) < ( deg ‘ 𝐺 ) ) )
70	9 4 10 69	syl3anc	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) = 0𝑝 ∨ ( deg ‘ ( 𝐻 ∘f − ( 𝐺 ∘f · ( 𝐻 quot 𝐺 ) ) ) ) < ( deg ‘ 𝐺 ) ) )
71	39 67 70	mpjaod	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = 0𝑝 )
72		df-0p	⊢ 0𝑝 = ( ℂ × { 0 } )
73	71 72	eqtrdi	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = ( ℂ × { 0 } ) )
74		ofsubeq0	⊢ ( ( ℂ ∈ V ∧ 𝐹 : ℂ ⟶ ℂ ∧ ( 𝐻 quot 𝐺 ) : ℂ ⟶ ℂ ) → ( ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = ( ℂ × { 0 } ) ↔ 𝐹 = ( 𝐻 quot 𝐺 ) ) )
75	18 20 29 74	syl3anc	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( ( 𝐹 ∘f − ( 𝐻 quot 𝐺 ) ) = ( ℂ × { 0 } ) ↔ 𝐹 = ( 𝐻 quot 𝐺 ) ) )
76	73 75	mpbid	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → 𝐹 = ( 𝐻 quot 𝐺 ) )
77	76	eqcomd	⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ∈ ( Poly ‘ 𝑆 ) ∧ 𝐺 ≠ 0𝑝 ) → ( 𝐻 quot 𝐺 ) = 𝐹 )