Metamath Proof Explorer

Theorem quotlem

Description: Lemma for properties of the polynomial quotient function. (Contributed by Mario Carneiro, 26-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 )
quotlem.8 
|- R = ( F oF - ( G oF x. ( F quot G ) ) )
Assertion quotlem 
|- ( ph -> ( ( F quot G ) e. ( Poly ` S ) /\ ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )

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 quotlem.8 
 |-  R = ( F oF - ( G oF x. ( F quot G ) ) )
9 eqid 
 |-  ( F oF - ( G oF x. q ) ) = ( F oF - ( G oF x. q ) )
10 9 quotval 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( F quot G ) = ( iota_ q e. ( Poly ` CC ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
11 5 6 7 10 syl3anc 
 |-  ( ph -> ( F quot G ) = ( iota_ q e. ( Poly ` CC ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
12 1 2 3 4 5 6 7 9 plydivalg 
 |-  ( ph -> E! q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) )
13 reurex 
 |-  ( E! q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) -> E. q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) )
14 12 13 syl 
 |-  ( ph -> E. q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) )
15 addcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
16 15 adantl 
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x + y ) e. CC )
17 mulcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x x. y ) e. CC )
18 17 adantl 
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x x. y ) e. CC )
19 reccl 
 |-  ( ( x e. CC /\ x =/= 0 ) -> ( 1 / x ) e. CC )
20 19 adantl 
 |-  ( ( ph /\ ( x e. CC /\ x =/= 0 ) ) -> ( 1 / x ) e. CC )
21 neg1cn 
 |-  -u 1 e. CC
22 21 a1i 
 |-  ( ph -> -u 1 e. CC )
23 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
24 23 5 sselid 
 |-  ( ph -> F e. ( Poly ` CC ) )
25 23 6 sselid 
 |-  ( ph -> G e. ( Poly ` CC ) )
26 16 18 20 22 24 25 7 9 plydivalg 
 |-  ( ph -> E! q e. ( Poly ` CC ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) )
27 id 
 |-  ( ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) -> ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) )
28 27 rgenw 
 |-  A. q e. ( Poly ` S ) ( ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) -> ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) )
29 riotass2 
 |-  ( ( ( ( Poly ` S ) C_ ( Poly ` CC ) /\ A. q e. ( Poly ` S ) ( ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) -> ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) /\ ( E. q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) /\ E! q e. ( Poly ` CC ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) ) -> ( iota_ q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) = ( iota_ q e. ( Poly ` CC ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
30 23 28 29 mpanl12 
 |-  ( ( E. q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) /\ E! q e. ( Poly ` CC ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) -> ( iota_ q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) = ( iota_ q e. ( Poly ` CC ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
31 14 26 30 syl2anc 
 |-  ( ph -> ( iota_ q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) = ( iota_ q e. ( Poly ` CC ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
32 11 31 eqtr4d 
 |-  ( ph -> ( F quot G ) = ( iota_ q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) )
33 riotacl2 
 |-  ( E! q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) -> ( iota_ q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) e. { q e. ( Poly ` S ) | ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) } )
34 12 33 syl 
 |-  ( ph -> ( iota_ q e. ( Poly ` S ) ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) ) e. { q e. ( Poly ` S ) | ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) } )
35 32 34 eqeltrd 
 |-  ( ph -> ( F quot G ) e. { q e. ( Poly ` S ) | ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) } )
36 oveq2 
 |-  ( q = ( F quot G ) -> ( G oF x. q ) = ( G oF x. ( F quot G ) ) )
37 36 oveq2d 
 |-  ( q = ( F quot G ) -> ( F oF - ( G oF x. q ) ) = ( F oF - ( G oF x. ( F quot G ) ) ) )
38 37 8 eqtr4di 
 |-  ( q = ( F quot G ) -> ( F oF - ( G oF x. q ) ) = R )
39 38 eqeq1d 
 |-  ( q = ( F quot G ) -> ( ( F oF - ( G oF x. q ) ) = 0p <-> R = 0p ) )
40 38 fveq2d 
 |-  ( q = ( F quot G ) -> ( deg ` ( F oF - ( G oF x. q ) ) ) = ( deg ` R ) )
41 40 breq1d 
 |-  ( q = ( F quot G ) -> ( ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) <-> ( deg ` R ) < ( deg ` G ) ) )
42 39 41 orbi12d 
 |-  ( q = ( F quot G ) -> ( ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) <-> ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
43 42 elrab 
 |-  ( ( F quot G ) e. { q e. ( Poly ` S ) | ( ( F oF - ( G oF x. q ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. q ) ) ) < ( deg ` G ) ) } <-> ( ( F quot G ) e. ( Poly ` S ) /\ ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
44 35 43 sylib 
 |-  ( ph -> ( ( F quot G ) e. ( Poly ` S ) /\ ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )