| Step |
Hyp |
Ref |
Expression |
| 1 |
|
deg1addle.y |
|- Y = ( Poly1 ` R ) |
| 2 |
|
deg1addle.d |
|- D = ( deg1 ` R ) |
| 3 |
|
deg1addle.r |
|- ( ph -> R e. Ring ) |
| 4 |
|
deg1suble.b |
|- B = ( Base ` Y ) |
| 5 |
|
deg1suble.m |
|- .- = ( -g ` Y ) |
| 6 |
|
deg1suble.f |
|- ( ph -> F e. B ) |
| 7 |
|
deg1suble.g |
|- ( ph -> G e. B ) |
| 8 |
|
deg1sub.l |
|- ( ph -> ( D ` G ) < ( D ` F ) ) |
| 9 |
|
eqid |
|- ( +g ` Y ) = ( +g ` Y ) |
| 10 |
|
eqid |
|- ( invg ` Y ) = ( invg ` Y ) |
| 11 |
4 9 10 5
|
grpsubval |
|- ( ( F e. B /\ G e. B ) -> ( F .- G ) = ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) ) |
| 12 |
6 7 11
|
syl2anc |
|- ( ph -> ( F .- G ) = ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) ) |
| 13 |
12
|
fveq2d |
|- ( ph -> ( D ` ( F .- G ) ) = ( D ` ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) ) ) |
| 14 |
1
|
ply1ring |
|- ( R e. Ring -> Y e. Ring ) |
| 15 |
|
ringgrp |
|- ( Y e. Ring -> Y e. Grp ) |
| 16 |
3 14 15
|
3syl |
|- ( ph -> Y e. Grp ) |
| 17 |
4 10
|
grpinvcl |
|- ( ( Y e. Grp /\ G e. B ) -> ( ( invg ` Y ) ` G ) e. B ) |
| 18 |
16 7 17
|
syl2anc |
|- ( ph -> ( ( invg ` Y ) ` G ) e. B ) |
| 19 |
1 2 3 4 10 7
|
deg1invg |
|- ( ph -> ( D ` ( ( invg ` Y ) ` G ) ) = ( D ` G ) ) |
| 20 |
19 8
|
eqbrtrd |
|- ( ph -> ( D ` ( ( invg ` Y ) ` G ) ) < ( D ` F ) ) |
| 21 |
1 2 3 4 9 6 18 20
|
deg1add |
|- ( ph -> ( D ` ( F ( +g ` Y ) ( ( invg ` Y ) ` G ) ) ) = ( D ` F ) ) |
| 22 |
13 21
|
eqtrd |
|- ( ph -> ( D ` ( F .- G ) ) = ( D ` F ) ) |