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

Metamath Proof Explorer

Theorem dvdsq1p

Description: Divisibility in a polynomial ring is witnessed by the quotient. (Contributed by Stefan O'Rear, 28-Mar-2015)

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

Proof

Step Hyp Ref Expression
1 dvdsq1p.p 
 |-  P = ( Poly1 ` R )
2 dvdsq1p.d 
 |-  .|| = ( ||r ` P )
3 dvdsq1p.b 
 |-  B = ( Base ` P )
4 dvdsq1p.c 
 |-  C = ( Unic1p ` R )
5 dvdsq1p.t 
 |-  .x. = ( .r ` P )
6 dvdsq1p.q 
 |-  Q = ( quot1p ` R )
7 1 3 4 uc1pcl 
 |-  ( G e. C -> G e. B )
8 7 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> G e. B )
9 3 2 5 dvdsr2 
 |-  ( G e. B -> ( G .|| F <-> E. q e. B ( q .x. G ) = F ) )
10 8 9 syl 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( G .|| F <-> E. q e. B ( q .x. G ) = F ) )
11 eqcom 
 |-  ( ( q .x. G ) = F <-> F = ( q .x. G ) )
12 simprr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> F = ( q .x. G ) )
13 simprl 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> q e. B )
14 simpl1 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ q e. B ) -> R e. Ring )
15 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
16 14 15 syl 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ q e. B ) -> P e. Ring )
17 ringgrp 
 |-  ( P e. Ring -> P e. Grp )
18 16 17 syl 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ q e. B ) -> P e. Grp )
19 simpl2 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ q e. B ) -> F e. B )
20 simpr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ q e. B ) -> q e. B )
21 8 adantr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ q e. B ) -> G e. B )
22 3 5 ringcl 
 |-  ( ( P e. Ring /\ q e. B /\ G e. B ) -> ( q .x. G ) e. B )
23 16 20 21 22 syl3anc 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ q e. B ) -> ( q .x. G ) e. B )
24 eqid 
 |-  ( 0g ` P ) = ( 0g ` P )
25 eqid 
 |-  ( -g ` P ) = ( -g ` P )
26 3 24 25 grpsubeq0 
 |-  ( ( P e. Grp /\ F e. B /\ ( q .x. G ) e. B ) -> ( ( F ( -g ` P ) ( q .x. G ) ) = ( 0g ` P ) <-> F = ( q .x. G ) ) )
27 18 19 23 26 syl3anc 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ q e. B ) -> ( ( F ( -g ` P ) ( q .x. G ) ) = ( 0g ` P ) <-> F = ( q .x. G ) ) )
28 27 biimprd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ q e. B ) -> ( F = ( q .x. G ) -> ( F ( -g ` P ) ( q .x. G ) ) = ( 0g ` P ) ) )
29 28 impr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> ( F ( -g ` P ) ( q .x. G ) ) = ( 0g ` P ) )
30 29 fveq2d 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> ( ( deg1 ` R ) ` ( F ( -g ` P ) ( q .x. G ) ) ) = ( ( deg1 ` R ) ` ( 0g ` P ) ) )
31 simpl1 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> R e. Ring )
32 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
33 32 1 24 deg1z 
 |-  ( R e. Ring -> ( ( deg1 ` R ) ` ( 0g ` P ) ) = -oo )
34 31 33 syl 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> ( ( deg1 ` R ) ` ( 0g ` P ) ) = -oo )
35 30 34 eqtrd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> ( ( deg1 ` R ) ` ( F ( -g ` P ) ( q .x. G ) ) ) = -oo )
36 32 4 uc1pdeg 
 |-  ( ( R e. Ring /\ G e. C ) -> ( ( deg1 ` R ) ` G ) e. NN0 )
37 36 3adant2 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( deg1 ` R ) ` G ) e. NN0 )
38 37 nn0red 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( deg1 ` R ) ` G ) e. RR )
39 38 adantr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> ( ( deg1 ` R ) ` G ) e. RR )
40 39 mnfltd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> -oo < ( ( deg1 ` R ) ` G ) )
41 35 40 eqbrtrd 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> ( ( deg1 ` R ) ` ( F ( -g ` P ) ( q .x. G ) ) ) < ( ( deg1 ` R ) ` G ) )
42 6 1 3 32 25 5 4 q1peqb 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( q e. B /\ ( ( deg1 ` R ) ` ( F ( -g ` P ) ( q .x. G ) ) ) < ( ( deg1 ` R ) ` G ) ) <-> ( F Q G ) = q ) )
43 42 adantr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> ( ( q e. B /\ ( ( deg1 ` R ) ` ( F ( -g ` P ) ( q .x. G ) ) ) < ( ( deg1 ` R ) ` G ) ) <-> ( F Q G ) = q ) )
44 13 41 43 mpbi2and 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> ( F Q G ) = q )
45 44 oveq1d 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> ( ( F Q G ) .x. G ) = ( q .x. G ) )
46 12 45 eqtr4d 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ ( q e. B /\ F = ( q .x. G ) ) ) -> F = ( ( F Q G ) .x. G ) )
47 46 expr 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ q e. B ) -> ( F = ( q .x. G ) -> F = ( ( F Q G ) .x. G ) ) )
48 11 47 biimtrid 
 |-  ( ( ( R e. Ring /\ F e. B /\ G e. C ) /\ q e. B ) -> ( ( q .x. G ) = F -> F = ( ( F Q G ) .x. G ) ) )
49 48 rexlimdva 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( E. q e. B ( q .x. G ) = F -> F = ( ( F Q G ) .x. G ) ) )
50 10 49 sylbid 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( G .|| F -> F = ( ( F Q G ) .x. G ) ) )
51 6 1 3 4 q1pcl 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F Q G ) e. B )
52 3 2 5 dvdsrmul 
 |-  ( ( G e. B /\ ( F Q G ) e. B ) -> G .|| ( ( F Q G ) .x. G ) )
53 8 51 52 syl2anc 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> G .|| ( ( F Q G ) .x. G ) )
54 breq2 
 |-  ( F = ( ( F Q G ) .x. G ) -> ( G .|| F <-> G .|| ( ( F Q G ) .x. G ) ) )
55 53 54 syl5ibrcom 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F = ( ( F Q G ) .x. G ) -> G .|| F ) )
56 50 55 impbid 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( G .|| F <-> F = ( ( F Q G ) .x. G ) ) )