Theorem deg1fvi

Description: Univariate polynomial degree respects protection. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Assertion	deg1fvi	|- ( deg1 ` R ) = ( deg1 ` ( _I ` R ) )

Proof

Step	Hyp	Ref	Expression
1		fvi	|- ( R e. _V -> ( _I ` R ) = R )
2	1	fveq2d	|- ( R e. _V -> ( deg1 ` ( _I ` R ) ) = ( deg1 ` R ) )
3		eqid	|- ( deg1 ` (/) ) = ( deg1 ` (/) )
4		eqid	|- ( Poly1 ` (/) ) = ( Poly1 ` (/) )
5		00ply1bas	|- (/) = ( Base ` ( Poly1 ` (/) ) )
6	3 4 5	deg1xrf	|- ( deg1 ` (/) ) : (/) --> RR*
7		ffn	|- ( ( deg1 ` (/) ) : (/) --> RR* -> ( deg1 ` (/) ) Fn (/) )
8	6 7	ax-mp	|- ( deg1 ` (/) ) Fn (/)
9		fn0	|- ( ( deg1 ` (/) ) Fn (/) <-> ( deg1 ` (/) ) = (/) )
10	8 9	mpbi	|- ( deg1 ` (/) ) = (/)
11		fvprc	|- ( -. R e. _V -> ( _I ` R ) = (/) )
12	11	fveq2d	|- ( -. R e. _V -> ( deg1 ` ( _I ` R ) ) = ( deg1 ` (/) ) )
13		fvprc	|- ( -. R e. _V -> ( deg1 ` R ) = (/) )
14	10 12 13	3eqtr4a	|- ( -. R e. _V -> ( deg1 ` ( _I ` R ) ) = ( deg1 ` R ) )
15	2 14	pm2.61i	|- ( deg1 ` ( _I ` R ) ) = ( deg1 ` R )
16	15	eqcomi	|- ( deg1 ` R ) = ( deg1 ` ( _I ` R ) )