Metamath Proof Explorer

Theorem r1pid

Description: Express the original polynomial F as F = ( q x. G ) + r using the quotient and remainder functions for q and r . (Contributed by Mario Carneiro, 5-Jun-2015)

Ref Expression
Hypotheses r1pid.p 
|- P = ( Poly1 ` R )
r1pid.b 
|- B = ( Base ` P )
r1pid.c 
|- C = ( Unic1p ` R )
r1pid.q 
|- Q = ( quot1p ` R )
r1pid.e 
|- E = ( rem1p ` R )
r1pid.t 
|- .x. = ( .r ` P )
r1pid.m 
|- .+ = ( +g ` P )
Assertion r1pid 
|- ( ( R e. Ring /\ F e. B /\ G e. C ) -> F = ( ( ( F Q G ) .x. G ) .+ ( F E G ) ) )

Proof

Step Hyp Ref Expression
1 r1pid.p 
 |-  P = ( Poly1 ` R )
2 r1pid.b 
 |-  B = ( Base ` P )
3 r1pid.c 
 |-  C = ( Unic1p ` R )
4 r1pid.q 
 |-  Q = ( quot1p ` R )
5 r1pid.e 
 |-  E = ( rem1p ` R )
6 r1pid.t 
 |-  .x. = ( .r ` P )
7 r1pid.m 
 |-  .+ = ( +g ` P )
8 1 2 3 uc1pcl 
 |-  ( G e. C -> G e. B )
9 eqid 
 |-  ( -g ` P ) = ( -g ` P )
10 5 1 2 4 6 9 r1pval 
 |-  ( ( F e. B /\ G e. B ) -> ( F E G ) = ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) )
11 8 10 sylan2 
 |-  ( ( F e. B /\ G e. C ) -> ( F E G ) = ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) )
12 11 3adant1 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F E G ) = ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) )
13 12 oveq2d 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( ( F Q G ) .x. G ) .+ ( F E G ) ) = ( ( ( F Q G ) .x. G ) .+ ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) ) )
14 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
15 14 3ad2ant1 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> P e. Ring )
16 ringabl 
 |-  ( P e. Ring -> P e. Abel )
17 15 16 syl 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> P e. Abel )
18 4 1 2 3 q1pcl 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F Q G ) e. B )
19 8 3ad2ant3 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> G e. B )
20 2 6 ringcl 
 |-  ( ( P e. Ring /\ ( F Q G ) e. B /\ G e. B ) -> ( ( F Q G ) .x. G ) e. B )
21 15 18 19 20 syl3anc 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( F Q G ) .x. G ) e. B )
22 ringgrp 
 |-  ( P e. Ring -> P e. Grp )
23 15 22 syl 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> P e. Grp )
24 simp2 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> F e. B )
25 2 9 grpsubcl 
 |-  ( ( P e. Grp /\ F e. B /\ ( ( F Q G ) .x. G ) e. B ) -> ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) e. B )
26 23 24 21 25 syl3anc 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) e. B )
27 2 7 ablcom 
 |-  ( ( P e. Abel /\ ( ( F Q G ) .x. G ) e. B /\ ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) e. B ) -> ( ( ( F Q G ) .x. G ) .+ ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) ) = ( ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) .+ ( ( F Q G ) .x. G ) ) )
28 17 21 26 27 syl3anc 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( ( F Q G ) .x. G ) .+ ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) ) = ( ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) .+ ( ( F Q G ) .x. G ) ) )
29 2 7 9 grpnpcan 
 |-  ( ( P e. Grp /\ F e. B /\ ( ( F Q G ) .x. G ) e. B ) -> ( ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) .+ ( ( F Q G ) .x. G ) ) = F )
30 23 24 21 29 syl3anc 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> ( ( F ( -g ` P ) ( ( F Q G ) .x. G ) ) .+ ( ( F Q G ) .x. G ) ) = F )
31 13 28 30 3eqtrrd 
 |-  ( ( R e. Ring /\ F e. B /\ G e. C ) -> F = ( ( ( F Q G ) .x. G ) .+ ( F E G ) ) )