Metamath Proof Explorer

Theorem quotval

Description: Value of the quotient function. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Hypothesis quotval.1 
|- R = ( F oF - ( G oF x. q ) )
Assertion quotval 
|- ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( F quot G ) = ( iota_ q e. ( Poly ` CC ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )

Proof

Step Hyp Ref Expression
1 quotval.1 
 |-  R = ( F oF - ( G oF x. q ) )
2 plyssc 
 |-  ( Poly ` S ) C_ ( Poly ` CC )
3 2 sseli 
 |-  ( F e. ( Poly ` S ) -> F e. ( Poly ` CC ) )
4 2 sseli 
 |-  ( G e. ( Poly ` S ) -> G e. ( Poly ` CC ) )
5 eldifsn 
 |-  ( G e. ( ( Poly ` CC ) \ { 0p } ) <-> ( G e. ( Poly ` CC ) /\ G =/= 0p ) )
6 oveq1 
 |-  ( g = G -> ( g oF x. q ) = ( G oF x. q ) )
7 oveq12 
 |-  ( ( f = F /\ ( g oF x. q ) = ( G oF x. q ) ) -> ( f oF - ( g oF x. q ) ) = ( F oF - ( G oF x. q ) ) )
8 6 7 sylan2 
 |-  ( ( f = F /\ g = G ) -> ( f oF - ( g oF x. q ) ) = ( F oF - ( G oF x. q ) ) )
9 8 1 eqtr4di 
 |-  ( ( f = F /\ g = G ) -> ( f oF - ( g oF x. q ) ) = R )
10 9 sbceq1d 
 |-  ( ( f = F /\ g = G ) -> ( [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) <-> [. R / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) ) )
11 1 ovexi 
 |-  R e. _V
12 eqeq1 
 |-  ( r = R -> ( r = 0p <-> R = 0p ) )
13 fveq2 
 |-  ( r = R -> ( deg ` r ) = ( deg ` R ) )
14 13 breq1d 
 |-  ( r = R -> ( ( deg ` r ) < ( deg ` g ) <-> ( deg ` R ) < ( deg ` g ) ) )
15 12 14 orbi12d 
 |-  ( r = R -> ( ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) <-> ( R = 0p \/ ( deg ` R ) < ( deg ` g ) ) ) )
16 11 15 sbcie 
 |-  ( [. R / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) <-> ( R = 0p \/ ( deg ` R ) < ( deg ` g ) ) )
17 simpr 
 |-  ( ( f = F /\ g = G ) -> g = G )
18 17 fveq2d 
 |-  ( ( f = F /\ g = G ) -> ( deg ` g ) = ( deg ` G ) )
19 18 breq2d 
 |-  ( ( f = F /\ g = G ) -> ( ( deg ` R ) < ( deg ` g ) <-> ( deg ` R ) < ( deg ` G ) ) )
20 19 orbi2d 
 |-  ( ( f = F /\ g = G ) -> ( ( R = 0p \/ ( deg ` R ) < ( deg ` g ) ) <-> ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
21 16 20 bitrid 
 |-  ( ( f = F /\ g = G ) -> ( [. R / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) <-> ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
22 10 21 bitrd 
 |-  ( ( f = F /\ g = G ) -> ( [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) <-> ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
23 22 riotabidv 
 |-  ( ( f = F /\ g = G ) -> ( iota_ q e. ( Poly ` CC ) [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) ) = ( iota_ q e. ( Poly ` CC ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
24 df-quot 
 |-  quot = ( f e. ( Poly ` CC ) , g e. ( ( Poly ` CC ) \ { 0p } ) |-> ( iota_ q e. ( Poly ` CC ) [. ( f oF - ( g oF x. q ) ) / r ]. ( r = 0p \/ ( deg ` r ) < ( deg ` g ) ) ) )
25 riotaex 
 |-  ( iota_ q e. ( Poly ` CC ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) e. _V
26 23 24 25 ovmpoa 
 |-  ( ( F e. ( Poly ` CC ) /\ G e. ( ( Poly ` CC ) \ { 0p } ) ) -> ( F quot G ) = ( iota_ q e. ( Poly ` CC ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
27 5 26 sylan2br 
 |-  ( ( F e. ( Poly ` CC ) /\ ( G e. ( Poly ` CC ) /\ G =/= 0p ) ) -> ( F quot G ) = ( iota_ q e. ( Poly ` CC ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
28 27 3impb 
 |-  ( ( F e. ( Poly ` CC ) /\ G e. ( Poly ` CC ) /\ G =/= 0p ) -> ( F quot G ) = ( iota_ q e. ( Poly ` CC ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
29 4 28 syl3an2 
 |-  ( ( F e. ( Poly ` CC ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( F quot G ) = ( iota_ q e. ( Poly ` CC ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )
30 3 29 syl3an1 
 |-  ( ( F e. ( Poly ` S ) /\ G e. ( Poly ` S ) /\ G =/= 0p ) -> ( F quot G ) = ( iota_ q e. ( Poly ` CC ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) ) )