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

Metamath Proof Explorer

Theorem plydiveu

Description: Lemma for plydivalg . (Contributed by Mario Carneiro, 24-Jul-2014)

Ref Expression
Hypotheses plydiv.pl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 + 𝑦 ) ∈ 𝑆 )
plydiv.tm ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 · 𝑦 ) ∈ 𝑆 )
plydiv.rc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ 𝑆 )
plydiv.m1 ⊢ ( 𝜑 → - 1 ∈ 𝑆 )
plydiv.f ⊢ ( 𝜑 → 𝐹 ∈ ( Poly ‘ 𝑆 ) )
plydiv.g ⊢ ( 𝜑 → 𝐺 ∈ ( Poly ‘ 𝑆 ) )
plydiv.z ⊢ ( 𝜑 → 𝐺 ≠ 0𝑝 )
plydiv.r ⊢ 𝑅 = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑞 ) )
plydiveu.q ⊢ ( 𝜑 → 𝑞 ∈ ( Poly ‘ 𝑆 ) )
plydiveu.qd ⊢ ( 𝜑 → ( 𝑅 = 0𝑝 ∨ ( deg ‘ 𝑅 ) < ( deg ‘ 𝐺 ) ) )
plydiveu.t ⊢ 𝑇 = ( 𝐹 ∘f − ( 𝐺 ∘f · 𝑝 ) )
plydiveu.p ⊢ ( 𝜑 → 𝑝 ∈ ( Poly ‘ 𝑆 ) )
plydiveu.pd ⊢ ( 𝜑 → ( 𝑇 = 0𝑝 ∨ ( deg ‘ 𝑇 ) < ( deg ‘ 𝐺 ) ) )
Assertion plydiveu ( 𝜑 → 𝑝 = 𝑞 )

Proof

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