Metamath Proof Explorer

Theorem plydivlem3

Description: Lemma for plydivex . Base case of induction. (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 ) )
plydiv.0 
|- ( ph -> ( F = 0p \/ ( ( deg ` F ) - ( deg ` G ) ) < 0 ) )
Assertion plydivlem3 
|- ( 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 plydiv.0 
 |-  ( ph -> ( F = 0p \/ ( ( deg ` F ) - ( deg ` G ) ) < 0 ) )
10 plybss 
 |-  ( F e. ( Poly ` S ) -> S C_ CC )
11 ply0 
 |-  ( S C_ CC -> 0p e. ( Poly ` S ) )
12 5 10 11 3syl 
 |-  ( ph -> 0p e. ( Poly ` S ) )
13 cnex 
 |-  CC e. _V
14 13 a1i 
 |-  ( ph -> CC e. _V )
15 plyf 
 |-  ( F e. ( Poly ` S ) -> F : CC --> CC )
16 ffn 
 |-  ( F : CC --> CC -> F Fn CC )
17 5 15 16 3syl 
 |-  ( ph -> F Fn CC )
18 plyf 
 |-  ( G e. ( Poly ` S ) -> G : CC --> CC )
19 ffn 
 |-  ( G : CC --> CC -> G Fn CC )
20 6 18 19 3syl 
 |-  ( ph -> G Fn CC )
21 plyf 
 |-  ( 0p e. ( Poly ` S ) -> 0p : CC --> CC )
22 ffn 
 |-  ( 0p : CC --> CC -> 0p Fn CC )
23 12 21 22 3syl 
 |-  ( ph -> 0p Fn CC )
24 inidm 
 |-  ( CC i^i CC ) = CC
25 20 23 14 14 24 offn 
 |-  ( ph -> ( G oF x. 0p ) Fn CC )
26 eqidd 
 |-  ( ( ph /\ z e. CC ) -> ( F ` z ) = ( F ` z ) )
27 eqidd 
 |-  ( ( ph /\ z e. CC ) -> ( G ` z ) = ( G ` z ) )
28 0pval 
 |-  ( z e. CC -> ( 0p ` z ) = 0 )
29 28 adantl 
 |-  ( ( ph /\ z e. CC ) -> ( 0p ` z ) = 0 )
30 20 23 14 14 24 27 29 ofval 
 |-  ( ( ph /\ z e. CC ) -> ( ( G oF x. 0p ) ` z ) = ( ( G ` z ) x. 0 ) )
31 6 18 syl 
 |-  ( ph -> G : CC --> CC )
32 31 ffvelrnda 
 |-  ( ( ph /\ z e. CC ) -> ( G ` z ) e. CC )
33 32 mul01d 
 |-  ( ( ph /\ z e. CC ) -> ( ( G ` z ) x. 0 ) = 0 )
34 30 33 eqtrd 
 |-  ( ( ph /\ z e. CC ) -> ( ( G oF x. 0p ) ` z ) = 0 )
35 5 15 syl 
 |-  ( ph -> F : CC --> CC )
36 35 ffvelrnda 
 |-  ( ( ph /\ z e. CC ) -> ( F ` z ) e. CC )
37 36 subid1d 
 |-  ( ( ph /\ z e. CC ) -> ( ( F ` z ) - 0 ) = ( F ` z ) )
38 14 17 25 17 26 34 37 offveq 
 |-  ( ph -> ( F oF - ( G oF x. 0p ) ) = F )
39 38 eqeq1d 
 |-  ( ph -> ( ( F oF - ( G oF x. 0p ) ) = 0p <-> F = 0p ) )
40 38 fveq2d 
 |-  ( ph -> ( deg ` ( F oF - ( G oF x. 0p ) ) ) = ( deg ` F ) )
41 dgrcl 
 |-  ( G e. ( Poly ` S ) -> ( deg ` G ) e. NN0 )
42 6 41 syl 
 |-  ( ph -> ( deg ` G ) e. NN0 )
43 42 nn0red 
 |-  ( ph -> ( deg ` G ) e. RR )
44 43 recnd 
 |-  ( ph -> ( deg ` G ) e. CC )
45 44 addid2d 
 |-  ( ph -> ( 0 + ( deg ` G ) ) = ( deg ` G ) )
46 45 eqcomd 
 |-  ( ph -> ( deg ` G ) = ( 0 + ( deg ` G ) ) )
47 40 46 breq12d 
 |-  ( ph -> ( ( deg ` ( F oF - ( G oF x. 0p ) ) ) < ( deg ` G ) <-> ( deg ` F ) < ( 0 + ( deg ` G ) ) ) )
48 dgrcl 
 |-  ( F e. ( Poly ` S ) -> ( deg ` F ) e. NN0 )
49 5 48 syl 
 |-  ( ph -> ( deg ` F ) e. NN0 )
50 49 nn0red 
 |-  ( ph -> ( deg ` F ) e. RR )
51 0red 
 |-  ( ph -> 0 e. RR )
52 50 43 51 ltsubaddd 
 |-  ( ph -> ( ( ( deg ` F ) - ( deg ` G ) ) < 0 <-> ( deg ` F ) < ( 0 + ( deg ` G ) ) ) )
53 47 52 bitr4d 
 |-  ( ph -> ( ( deg ` ( F oF - ( G oF x. 0p ) ) ) < ( deg ` G ) <-> ( ( deg ` F ) - ( deg ` G ) ) < 0 ) )
54 39 53 orbi12d 
 |-  ( ph -> ( ( ( F oF - ( G oF x. 0p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. 0p ) ) ) < ( deg ` G ) ) <-> ( F = 0p \/ ( ( deg ` F ) - ( deg ` G ) ) < 0 ) ) )
55 9 54 mpbird 
 |-  ( ph -> ( ( F oF - ( G oF x. 0p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. 0p ) ) ) < ( deg ` G ) ) )
56 oveq2 
 |-  ( q = 0p -> ( G oF x. q ) = ( G oF x. 0p ) )
57 56 oveq2d 
 |-  ( q = 0p -> ( F oF - ( G oF x. q ) ) = ( F oF - ( G oF x. 0p ) ) )
58 8 57 syl5eq 
 |-  ( q = 0p -> R = ( F oF - ( G oF x. 0p ) ) )
59 58 eqeq1d 
 |-  ( q = 0p -> ( R = 0p <-> ( F oF - ( G oF x. 0p ) ) = 0p ) )
60 58 fveq2d 
 |-  ( q = 0p -> ( deg ` R ) = ( deg ` ( F oF - ( G oF x. 0p ) ) ) )
61 60 breq1d 
 |-  ( q = 0p -> ( ( deg ` R ) < ( deg ` G ) <-> ( deg ` ( F oF - ( G oF x. 0p ) ) ) < ( deg ` G ) ) )
62 59 61 orbi12d 
 |-  ( q = 0p -> ( ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) <-> ( ( F oF - ( G oF x. 0p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. 0p ) ) ) < ( deg ` G ) ) ) )
63 62 rspcev 
 |-  ( ( 0p e. ( Poly ` S ) /\ ( ( F oF - ( G oF x. 0p ) ) = 0p \/ ( deg ` ( F oF - ( G oF x. 0p ) ) ) < ( deg ` G ) ) ) -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) )
64 12 55 63 syl2anc 
 |-  ( ph -> E. q e. ( Poly ` S ) ( R = 0p \/ ( deg ` R ) < ( deg ` G ) ) )