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 ) ) )