This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐺 ) = 𝐹 )