Metamath Proof Explorer

Theorem plydiveu

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

Ref Expression
Hypotheses plydiv.pl 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
plydiv.tm 
|- ( ( ph /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
plydiv.rc 
|- ( ( ph /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )
plydiv.m1 
|- ( ph -> -u 1 e. S )
plydiv.f 
|- ( ph -> F e. ( Poly ` S ) )
plydiv.g 
|- ( ph -> G e. ( Poly ` S ) )
plydiv.z 
|- ( ph -> G =/= 0p )
plydiv.r 
|- R = ( F oF - ( G oF x. q ) )
plydiveu.q 
|- ( ph -> q e. ( Poly ` S ) )
plydiveu.qd 
|- ( ph -> ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) )
plydiveu.t 
|- T = ( F oF - ( G oF x. p ) )
plydiveu.p 
|- ( ph -> p e. ( Poly ` S ) )
plydiveu.pd 
|- ( ph -> ( T = 0p \/ ( deg ` T ) < ( deg ` G ) ) )
Assertion plydiveu 
|- ( ph -> p = q )

Proof

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