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	⊢ ( 𝜑 → 𝑝 = 𝑞 )