deg1submon1p

Description: The difference of two monic polynomials of the same degree is a polynomial of lesser degree. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	deg1submon1p.d	\|- D = ( deg1 ` R )
	deg1submon1p.o	\|- O = ( Monic1p ` R )
	deg1submon1p.p	\|- P = ( Poly1 ` R )
	deg1submon1p.m	\|- .- = ( -g ` P )
	deg1submon1p.r	\|- ( ph -> R e. Ring )
	deg1submon1p.f1	\|- ( ph -> F e. O )
	deg1submon1p.f2	\|- ( ph -> ( D ` F ) = X )
	deg1submon1p.g1	\|- ( ph -> G e. O )
	deg1submon1p.g2	\|- ( ph -> ( D ` G ) = X )
Assertion	deg1submon1p	\|- ( ph -> ( D ` ( F .- G ) ) < X )

Proof

Step	Hyp	Ref	Expression
1		deg1submon1p.d	\|- D = ( deg1 ` R )
2		deg1submon1p.o	\|- O = ( Monic1p ` R )
3		deg1submon1p.p	\|- P = ( Poly1 ` R )
4		deg1submon1p.m	\|- .- = ( -g ` P )
5		deg1submon1p.r	\|- ( ph -> R e. Ring )
6		deg1submon1p.f1	\|- ( ph -> F e. O )
7		deg1submon1p.f2	\|- ( ph -> ( D ` F ) = X )
8		deg1submon1p.g1	\|- ( ph -> G e. O )
9		deg1submon1p.g2	\|- ( ph -> ( D ` G ) = X )
10		eqid	\|- ( Base ` P ) = ( Base ` P )
11	3 10 2	mon1pcl	\|- ( F e. O -> F e. ( Base ` P ) )
12	6 11	syl	\|- ( ph -> F e. ( Base ` P ) )
13		eqid	\|- ( 0g ` P ) = ( 0g ` P )
14	3 13 2	mon1pn0	\|- ( F e. O -> F =/= ( 0g ` P ) )
15	6 14	syl	\|- ( ph -> F =/= ( 0g ` P ) )
16	1 3 13 10	deg1nn0cl	\|- ( ( R e. Ring /\ F e. ( Base ` P ) /\ F =/= ( 0g ` P ) ) -> ( D ` F ) e. NN0 )
17	5 12 15 16	syl3anc	\|- ( ph -> ( D ` F ) e. NN0 )
18	7 17	eqeltrrd	\|- ( ph -> X e. NN0 )
19	18	nn0red	\|- ( ph -> X e. RR )
20	19	leidd	\|- ( ph -> X <_ X )
21	7 20	eqbrtrd	\|- ( ph -> ( D ` F ) <_ X )
22	3 10 2	mon1pcl	\|- ( G e. O -> G e. ( Base ` P ) )
23	8 22	syl	\|- ( ph -> G e. ( Base ` P ) )
24	9 20	eqbrtrd	\|- ( ph -> ( D ` G ) <_ X )
25		eqid	\|- ( coe1 ` F ) = ( coe1 ` F )
26		eqid	\|- ( coe1 ` G ) = ( coe1 ` G )
27	7	fveq2d	\|- ( ph -> ( ( coe1 ` F ) ` ( D ` F ) ) = ( ( coe1 ` F ) ` X ) )
28		eqid	\|- ( 1r ` R ) = ( 1r ` R )
29	1 28 2	mon1pldg	\|- ( F e. O -> ( ( coe1 ` F ) ` ( D ` F ) ) = ( 1r ` R ) )
30	6 29	syl	\|- ( ph -> ( ( coe1 ` F ) ` ( D ` F ) ) = ( 1r ` R ) )
31	27 30	eqtr3d	\|- ( ph -> ( ( coe1 ` F ) ` X ) = ( 1r ` R ) )
32	1 28 2	mon1pldg	\|- ( G e. O -> ( ( coe1 ` G ) ` ( D ` G ) ) = ( 1r ` R ) )
33	8 32	syl	\|- ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) = ( 1r ` R ) )
34	9	fveq2d	\|- ( ph -> ( ( coe1 ` G ) ` ( D ` G ) ) = ( ( coe1 ` G ) ` X ) )
35	31 33 34	3eqtr2d	\|- ( ph -> ( ( coe1 ` F ) ` X ) = ( ( coe1 ` G ) ` X ) )
36	1 3 10 4 18 5 12 21 23 24 25 26 35	deg1sublt	\|- ( ph -> ( D ` ( F .- G ) ) < X )

Metamath Proof Explorer

Theorem deg1submon1p

Proof