Metamath Proof Explorer

Theorem quotcan

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

Ref Expression
Hypothesis quotcan.1 
|- H = ( F oF x. G )
Assertion quotcan 
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( H quot G ) = F )

Proof

Step Hyp Ref Expression
1 quotcan.1 
 |-  H = ( F oF x. G )
2 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
3 simp2 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> G e. ( Poly ` S ) )
4 2 3 sselid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> G e. ( Poly ` CC ) )
5 simp1 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> F e. ( Poly ` S ) )
6 2 5 sselid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> F e. ( Poly ` CC ) )
7 plymulcl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> ( F oF x. G ) e. ( Poly ` CC ) )
8 1 7 eqeltrid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) ) -> H e. ( Poly ` CC ) )
9 8 3adant3 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> H e. ( Poly ` CC ) )
10 simp3 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> G =/= 0p )
11 quotcl2 
 |-  ( ( H e. ( Poly ` CC ) /\ G e. ( Poly ` CC ) /\ G =/= 0p ) -> ( H quot G ) e. ( Poly ` CC ) )
12 9 4 10 11 syl3anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( H quot G ) e. ( Poly ` CC ) )
13 plysubcl 
 |-  ( ( F e. ( Poly ` CC ) /\ ( H quot G ) e. ( Poly ` CC ) ) -> ( F oF - ( H quot G ) ) e. ( Poly ` CC ) )
14 6 12 13 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( F oF - ( H quot G ) ) e. ( Poly ` CC ) )
15 plymul0or 
 |-  ( ( G e. ( Poly ` CC ) /\ ( F oF - ( H quot G ) ) e. ( Poly ` CC ) ) -> ( ( G oF x. ( F oF - ( H quot G ) ) ) = 0p <-> ( G = 0p \/ ( F oF - ( H quot G ) ) = 0p ) ) )
16 4 14 15 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( G oF x. ( F oF - ( H quot G ) ) ) = 0p <-> ( G = 0p \/ ( F oF - ( H quot G ) ) = 0p ) ) )
17 cnex 
 |-  CC e. _V
18 17 a1i 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> CC e. _V )
19 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
20 5 19 syl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> F : CC --> CC )
21 plyf 
 |-  ( G e. ( Poly ` S ) -> G : CC --> CC )
22 3 21 syl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> G : CC --> CC )
23 mulcom 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) = ( y x. x ) )
24 23 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) = ( y x. x ) )
25 18 20 22 24 caofcom 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( F oF x. G ) = ( G oF x. F ) )
26 1 25 eqtrid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> H = ( G oF x. F ) )
27 26 oveq1d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( H oF - ( G oF x. ( H quot G ) ) ) = ( ( G oF x. F ) oF - ( G oF x. ( H quot G ) ) ) )
28 plyf 
 |-  ( ( H quot G ) e. ( Poly ` CC ) -> ( H quot G ) : CC --> CC )
29 12 28 syl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( H quot G ) : CC --> CC )
30 subdi 
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( x x. ( y - z ) ) = ( ( x x. y ) - ( x x. z ) ) )
31 30 adantl 
 |-  ( ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( x x. ( y - z ) ) = ( ( x x. y ) - ( x x. z ) ) )
32 18 22 20 29 31 caofdi 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( G oF x. ( F oF - ( H quot G ) ) ) = ( ( G oF x. F ) oF - ( G oF x. ( H quot G ) ) ) )
33 27 32 eqtr4d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( H oF - ( G oF x. ( H quot G ) ) ) = ( G oF x. ( F oF - ( H quot G ) ) ) )
34 33 eqeq1d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( H oF - ( G oF x. ( H quot G ) ) ) = 0p <-> ( G oF x. ( F oF - ( H quot G ) ) ) = 0p ) )
35 10 neneqd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> -. G = 0p )
36 biorf 
 |-  ( -. G = 0p -> ( ( F oF - ( H quot G ) ) = 0p <-> ( G = 0p \/ ( F oF - ( H quot G ) ) = 0p ) ) )
37 35 36 syl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( F oF - ( H quot G ) ) = 0p <-> ( G = 0p \/ ( F oF - ( H quot G ) ) = 0p ) ) )
38 16 34 37 3bitr4d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( H oF - ( G oF x. ( H quot G ) ) ) = 0p <-> ( F oF - ( H quot G ) ) = 0p ) )
39 38 biimpd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( H oF - ( G oF x. ( H quot G ) ) ) = 0p -> ( F oF - ( H quot G ) ) = 0p ) )
40 eqid 
 |-  ( deg ` G ) = ( deg ` G )
41 eqid 
 |-  ( deg ` ( F oF - ( H quot G ) ) ) = ( deg ` ( F oF - ( H quot G ) ) )
42 40 41 dgrmul 
 |-  ( ( ( G e. ( Poly ` CC ) /\ G =/= 0p ) /\ ( ( F oF - ( H quot G ) ) e. ( Poly ` CC ) /\ ( F oF - ( H quot G ) ) =/= 0p ) ) -> ( deg ` ( G oF x. ( F oF - ( H quot G ) ) ) ) = ( ( deg ` G ) + ( deg ` ( F oF - ( H quot G ) ) ) ) )
43 42 expr 
 |-  ( ( ( G e. ( Poly ` CC ) /\ G =/= 0p ) /\ ( F oF - ( H quot G ) ) e. ( Poly ` CC ) ) -> ( ( F oF - ( H quot G ) ) =/= 0p -> ( deg ` ( G oF x. ( F oF - ( H quot G ) ) ) ) = ( ( deg ` G ) + ( deg ` ( F oF - ( H quot G ) ) ) ) ) )
44 4 10 14 43 syl21anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( F oF - ( H quot G ) ) =/= 0p -> ( deg ` ( G oF x. ( F oF - ( H quot G ) ) ) ) = ( ( deg ` G ) + ( deg ` ( F oF - ( H quot G ) ) ) ) ) )
45 dgrcl 
 |-  ( G e. ( Poly ` S ) -> ( deg ` G ) e. NN0 )
46 3 45 syl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( deg ` G ) e. NN0 )
47 46 nn0red 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( deg ` G ) e. RR )
48 dgrcl 
 |-  ( ( F oF - ( H quot G ) ) e. ( Poly ` CC ) -> ( deg ` ( F oF - ( H quot G ) ) ) e. NN0 )
49 14 48 syl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( deg ` ( F oF - ( H quot G ) ) ) e. NN0 )
50 nn0addge1 
 |-  ( ( ( deg ` G ) e. RR /\ ( deg ` ( F oF - ( H quot G ) ) ) e. NN0 ) -> ( deg ` G ) <_ ( ( deg ` G ) + ( deg ` ( F oF - ( H quot G ) ) ) ) )
51 47 49 50 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( deg ` G ) <_ ( ( deg ` G ) + ( deg ` ( F oF - ( H quot G ) ) ) ) )
52 breq2 
 |-  ( ( deg ` ( G oF x. ( F oF - ( H quot G ) ) ) ) = ( ( deg ` G ) + ( deg ` ( F oF - ( H quot G ) ) ) ) -> ( ( deg ` G ) <_ ( deg ` ( G oF x. ( F oF - ( H quot G ) ) ) ) <-> ( deg ` G ) <_ ( ( deg ` G ) + ( deg ` ( F oF - ( H quot G ) ) ) ) ) )
53 51 52 syl5ibrcom 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( deg ` ( G oF x. ( F oF - ( H quot G ) ) ) ) = ( ( deg ` G ) + ( deg ` ( F oF - ( H quot G ) ) ) ) -> ( deg ` G ) <_ ( deg ` ( G oF x. ( F oF - ( H quot G ) ) ) ) ) )
54 44 53 syld 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( F oF - ( H quot G ) ) =/= 0p -> ( deg ` G ) <_ ( deg ` ( G oF x. ( F oF - ( H quot G ) ) ) ) ) )
55 33 fveq2d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( deg ` ( H oF - ( G oF x. ( H quot G ) ) ) ) = ( deg ` ( G oF x. ( F oF - ( H quot G ) ) ) ) )
56 55 breq2d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( deg ` G ) <_ ( deg ` ( H oF - ( G oF x. ( H quot G ) ) ) ) <-> ( deg ` G ) <_ ( deg ` ( G oF x. ( F oF - ( H quot G ) ) ) ) ) )
57 plymulcl 
 |-  ( ( G e. ( Poly ` CC ) /\ ( H quot G ) e. ( Poly ` CC ) ) -> ( G oF x. ( H quot G ) ) e. ( Poly ` CC ) )
58 4 12 57 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( G oF x. ( H quot G ) ) e. ( Poly ` CC ) )
59 plysubcl 
 |-  ( ( H e. ( Poly ` CC ) /\ ( G oF x. ( H quot G ) ) e. ( Poly ` CC ) ) -> ( H oF - ( G oF x. ( H quot G ) ) ) e. ( Poly ` CC ) )
60 9 58 59 syl2anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( H oF - ( G oF x. ( H quot G ) ) ) e. ( Poly ` CC ) )
61 dgrcl 
 |-  ( ( H oF - ( G oF x. ( H quot G ) ) ) e. ( Poly ` CC ) -> ( deg ` ( H oF - ( G oF x. ( H quot G ) ) ) ) e. NN0 )
62 60 61 syl 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( deg ` ( H oF - ( G oF x. ( H quot G ) ) ) ) e. NN0 )
63 62 nn0red 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( deg ` ( H oF - ( G oF x. ( H quot G ) ) ) ) e. RR )
64 47 63 lenltd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( deg ` G ) <_ ( deg ` ( H oF - ( G oF x. ( H quot G ) ) ) ) <-> -. ( deg ` ( H oF - ( G oF x. ( H quot G ) ) ) ) < ( deg ` G ) ) )
65 56 64 bitr3d 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( deg ` G ) <_ ( deg ` ( G oF x. ( F oF - ( H quot G ) ) ) ) <-> -. ( deg ` ( H oF - ( G oF x. ( H quot G ) ) ) ) < ( deg ` G ) ) )
66 54 65 sylibd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( F oF - ( H quot G ) ) =/= 0p -> -. ( deg ` ( H oF - ( G oF x. ( H quot G ) ) ) ) < ( deg ` G ) ) )
67 66 necon4ad 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( deg ` ( H oF - ( G oF x. ( H quot G ) ) ) ) < ( deg ` G ) -> ( F oF - ( H quot G ) ) = 0p ) )
68 eqid 
 |-  ( H oF - ( G oF x. ( H quot G ) ) ) = ( H oF - ( G oF x. ( H quot G ) ) )
69 68 quotdgr 
 |-  ( ( H e. ( Poly ` CC ) /\ G e. ( Poly ` CC ) /\ G =/= 0p ) -> ( ( H oF - ( G oF x. ( H quot G ) ) ) = 0p \/ ( deg ` ( H oF - ( G oF x. ( H quot G ) ) ) ) < ( deg ` G ) ) )
70 9 4 10 69 syl3anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( H oF - ( G oF x. ( H quot G ) ) ) = 0p \/ ( deg ` ( H oF - ( G oF x. ( H quot G ) ) ) ) < ( deg ` G ) ) )
71 39 67 70 mpjaod 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( F oF - ( H quot G ) ) = 0p )
72 df-0p 
 |-  0p = ( CC X. { 0 } )
73 71 72 eqtrdi 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( F oF - ( H quot G ) ) = ( CC X. { 0 } ) )
74 ofsubeq0 
 |-  ( ( CC e. _V /\ F : CC --> CC /\ ( H quot G ) : CC --> CC ) -> ( ( F oF - ( H quot G ) ) = ( CC X. { 0 } ) <-> F = ( H quot G ) ) )
75 18 20 29 74 syl3anc 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( ( F oF - ( H quot G ) ) = ( CC X. { 0 } ) <-> F = ( H quot G ) ) )
76 73 75 mpbid 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> F = ( H quot G ) )
77 76 eqcomd 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( H quot G ) = F )