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

Metamath Proof Explorer

Theorem plydivalg

Description: The division algorithm on polynomials over a subfield S of the complex numbers. If F and G =/= 0 are polynomials over S , then there is a unique quotient polynomial q such that the remainder F - G x. q is either zero or has degree less than G . (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 )
plydiv.r 
|- R = ( F oF - ( G oF x. q ) )
Assertion plydivalg 
|- ( ph -> E! q 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 plydiv.r 
 |-  R = ( F oF - ( G oF x. q ) )
9 1 2 3 4 5 6 7 8 plydivex 
 |-  ( ph -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) )
10 simpll 
 |-  ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) -> ph )
11 10 1 sylan 
 |-  ( ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x + y ) e. S )
12 10 2 sylan 
 |-  ( ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) /\ ( x e. S /\ y e. S ) ) -> ( x x. y ) e. S )
13 10 3 sylan 
 |-  ( ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) /\ ( x e. S /\ x =/= 0 ) ) -> ( 1 / x ) e. S )
14 10 4 syl 
 |-  ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) -> -u 1 e. S )
15 10 5 syl 
 |-  ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) -> F e. ( Poly ` S ) )
16 10 6 syl 
 |-  ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) -> G e. ( Poly ` S ) )
17 10 7 syl 
 |-  ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) -> G =/= 0p )
18 eqid 
 |-  ( F oF - ( G oF x. p ) ) = ( F oF - ( G oF x. p ) )
19 simplrr 
 |-  ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) -> p e. ( Poly ` S ) )
20 simprr 
 |-  ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) -> ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) )
21 simplrl 
 |-  ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) -> q e. ( Poly ` S ) )
22 simprl 
 |-  ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) -> ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) )
23 11 12 13 14 15 16 17 18 19 20 8 21 22 plydiveu 
 |-  ( ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) /\ ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) ) -> q = p )
24 23 ex 
 |-  ( ( ph /\ ( q e. ( Poly ` S ) /\ p e. ( Poly ` S ) ) ) -> ( ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) -> q = p ) )
25 24 ralrimivva 
 |-  ( ph -> A. q e. ( Poly ` S ) A. p e. ( Poly ` S ) ( ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) -> q = p ) )
26 oveq2 
 |-  ( q = p -> ( G oF x. q ) = ( G oF x. p ) )
27 26 oveq2d 
 |-  ( q = p -> ( F oF - ( G oF x. q ) ) = ( F oF - ( G oF x. p ) ) )
28 8 27 eqtrid 
 |-  ( q = p -> R = ( F oF - ( G oF x. p ) ) )
29 28 eqeq1d 
 |-  ( q = p -> ( R = 0p <-> ( F oF - ( G oF x. p ) ) = 0p ) )
30 28 fveq2d 
 |-  ( q = p -> ( deg ` R ) = ( deg ` ( F oF - ( G oF x. p ) ) ) )
31 30 breq1d 
 |-  ( q = p -> ( ( deg ` R ) < ( deg ` G ) <-> ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) )
32 29 31 orbi12d 
 |-  ( q = p -> ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) <-> ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) )
33 32 reu4 
 |-  ( E! q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) <-> ( E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ A. q e. ( Poly ` S ) A. p e. ( Poly ` S ) ( ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) /\ ( ( F oF - ( G oF x. p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. p ) ) ) < ( deg ` G ) ) ) -> q = p ) ) )
34 9 25 33 sylanbrc 
 |-  ( ph -> E! q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) )