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