Metamath Proof Explorer

Theorem q1peqb

Description: Characterizing property of the polynomial quotient. (Contributed by Stefan O'Rear, 28-Mar-2015)

Ref Expression
Hypotheses q1pval.q 
|- Q = ( quot1p ` R )
q1pval.p 
|- P = ( Poly1 ` R )
q1pval.b 
|- B = ( Base ` P )
q1pval.d 
|- D = ( deg1 ` R )
q1pval.m 
|- .- = ( -g ` P )
q1pval.t 
|- .x. = ( .r ` P )
q1peqb.c 
|- C = ( Unic1p ` R )
Assertion q1peqb 
|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( X e. B /\ ( D ` ( F .- ( X .x. G ) ) ) < ( D ` G ) ) <-> ( F Q G ) = X ) )

Proof

Step Hyp Ref Expression
1 q1pval.q 
 |-  Q = ( quot1p ` R )
2 q1pval.p 
 |-  P = ( Poly1 ` R )
3 q1pval.b 
 |-  B = ( Base ` P )
4 q1pval.d 
 |-  D = ( deg1 ` R )
5 q1pval.m 
 |-  .- = ( -g ` P )
6 q1pval.t 
 |-  .x. = ( .r ` P )
7 q1peqb.c 
 |-  C = ( Unic1p ` R )
8 elex 
 |-  ( X e. B -> X e. _V )
9 8 adantr 
 |-  ( ( X e. B /\ ( D ` ( F .- ( X .x. G ) ) ) < ( D ` G ) ) -> X e. _V )
10 9 a1i 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( X e. B /\ ( D ` ( F .- ( X .x. G ) ) ) < ( D ` G ) ) -> X e. _V ) )
11 ovex 
 |-  ( F Q G ) e. _V
12 eleq1 
 |-  ( ( F Q G ) = X -> ( ( F Q G ) e. _V <-> X e. _V ) )
13 11 12 mpbii 
 |-  ( ( F Q G ) = X -> X e. _V )
14 13 a1i 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( F Q G ) = X -> X e. _V ) )
15 simpr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ X e. _V ) -> X e. _V )
16 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
17 simp1 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> R e. Ring )
18 simp2 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> F e. B )
19 2 3 7 uc1pcl 
 |-  ( G e. C -> G e. B )
20 19 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> G e. B )
21 2 16 7 uc1pn0 
 |-  ( G e. C -> G =/= ( 0g ` P ) )
22 21 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> G =/= ( 0g ` P ) )
23 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
24 4 23 7 uc1pldg 
 |-  ( G e. C -> ( ( coe1 ` G ) ` ( D ` G ) ) e. ( Unit ` R ) )
25 24 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( coe1 ` G ) ` ( D ` G ) ) e. ( Unit ` R ) )
26 2 4 3 5 16 6 17 18 20 22 25 23 ply1divalg2 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> E! q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) )
27 df-reu 
 |-  ( E! q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) <-> E! q ( q e. B /\ ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )
28 26 27 sylib 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> E! q ( q e. B /\ ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )
29 28 adantr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ X e. _V ) -> E! q ( q e. B /\ ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )
30 eleq1 
 |-  ( q = X -> ( q e. B <-> X e. B ) )
31 oveq1 
 |-  ( q = X -> ( q .x. G ) = ( X .x. G ) )
32 31 oveq2d 
 |-  ( q = X -> ( F .- ( q .x. G ) ) = ( F .- ( X .x. G ) ) )
33 32 fveq2d 
 |-  ( q = X -> ( D ` ( F .- ( q .x. G ) ) ) = ( D ` ( F .- ( X .x. G ) ) ) )
34 33 breq1d 
 |-  ( q = X -> ( ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) <-> ( D ` ( F .- ( X .x. G ) ) ) < ( D ` G ) ) )
35 30 34 anbi12d 
 |-  ( q = X -> ( ( q e. B /\ ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) <-> ( X e. B /\ ( D ` ( F .- ( X .x. G ) ) ) < ( D ` G ) ) ) )
36 35 adantl 
 |-  ( ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ X e. _V ) /\ q = X ) -> ( ( q e. B /\ ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) <-> ( X e. B /\ ( D ` ( F .- ( X .x. G ) ) ) < ( D ` G ) ) ) )
37 15 29 36 iota2d 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ X e. _V ) -> ( ( X e. B /\ ( D ` ( F .- ( X .x. G ) ) ) < ( D ` G ) ) <-> ( iota q ( q e. B /\ ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) ) = X ) )
38 1 2 3 4 5 6 q1pval 
 |-  ( ( F e. B /\ G e. B ) -> ( F Q G ) = ( iota_ q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )
39 18 20 38 syl2anc 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F Q G ) = ( iota_ q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )
40 df-riota 
 |-  ( iota_ q e. B ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) = ( iota q ( q e. B /\ ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) )
41 39 40 eqtrdi 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F Q G ) = ( iota q ( q e. B /\ ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) ) )
42 41 adantr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ X e. _V ) -> ( F Q G ) = ( iota q ( q e. B /\ ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) ) )
43 42 eqeq1d 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ X e. _V ) -> ( ( F Q G ) = X <-> ( iota q ( q e. B /\ ( D ` ( F .- ( q .x. G ) ) ) < ( D ` G ) ) ) = X ) )
44 37 43 bitr4d 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ X e. _V ) -> ( ( X e. B /\ ( D ` ( F .- ( X .x. G ) ) ) < ( D ` G ) ) <-> ( F Q G ) = X ) )
45 44 ex 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( X e. _V -> ( ( X e. B /\ ( D ` ( F .- ( X .x. G ) ) ) < ( D ` G ) ) <-> ( F Q G ) = X ) ) )
46 10 14 45 pm5.21ndd 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( X e. B /\ ( D ` ( F .- ( X .x. G ) ) ) < ( D ` G ) ) <-> ( F Q G ) = X ) )