deg1invg

Description: The degree of the negated polynomial is the same as the original. (Contributed by Stefan O'Rear, 28-Mar-2015)

	Ref	Expression
Hypotheses	deg1addle.y	\|- Y = ( Poly1 ` R )
	deg1addle.d	\|- D = ( deg1 ` R )
	deg1addle.r	\|- ( ph -> R e. Ring )
	deg1invg.b	\|- B = ( Base ` Y )
	deg1invg.n	\|- N = ( invg ` Y )
	deg1invg.f	\|- ( ph -> F e. B )
Assertion	deg1invg	\|- ( ph -> ( D ` ( N ` F ) ) = ( D ` F ) )

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	\|- Y = ( Poly1 ` R )
2		deg1addle.d	\|- D = ( deg1 ` R )
3		deg1addle.r	\|- ( ph -> R e. Ring )
4		deg1invg.b	\|- B = ( Base ` Y )
5		deg1invg.n	\|- N = ( invg ` Y )
6		deg1invg.f	\|- ( ph -> F e. B )
7	1	ply1lmod	\|- ( R e. Ring -> Y e. LMod )
8	3 7	syl	\|- ( ph -> Y e. LMod )
9	1	ply1sca2	\|- ( _I ` R ) = ( Scalar ` Y )
10		eqid	\|- ( .s ` Y ) = ( .s ` Y )
11		eqid	\|- ( 1r ` ( _I ` R ) ) = ( 1r ` ( _I ` R ) )
12		eqid	\|- ( invg ` R ) = ( invg ` R )
13	12	grpinvfvi	\|- ( invg ` R ) = ( invg ` ( _I ` R ) )
14	4 5 9 10 11 13	lmodvneg1	\|- ( ( Y e. LMod /\ F e. B ) -> ( ( ( invg ` R ) ` ( 1r ` ( _I ` R ) ) ) ( .s ` Y ) F ) = ( N ` F ) )
15	8 6 14	syl2anc	\|- ( ph -> ( ( ( invg ` R ) ` ( 1r ` ( _I ` R ) ) ) ( .s ` Y ) F ) = ( N ` F ) )
16	15	fveq2d	\|- ( ph -> ( D ` ( ( ( invg ` R ) ` ( 1r ` ( _I ` R ) ) ) ( .s ` Y ) F ) ) = ( D ` ( N ` F ) ) )
17		eqid	\|- ( RLReg ` R ) = ( RLReg ` R )
18		fvi	\|- ( R e. Ring -> ( _I ` R ) = R )
19	3 18	syl	\|- ( ph -> ( _I ` R ) = R )
20	19	fveq2d	\|- ( ph -> ( 1r ` ( _I ` R ) ) = ( 1r ` R ) )
21	20	fveq2d	\|- ( ph -> ( ( invg ` R ) ` ( 1r ` ( _I ` R ) ) ) = ( ( invg ` R ) ` ( 1r ` R ) ) )
22		eqid	\|- ( Unit ` R ) = ( Unit ` R )
23	17 22	unitrrg	\|- ( R e. Ring -> ( Unit ` R ) C_ ( RLReg ` R ) )
24	3 23	syl	\|- ( ph -> ( Unit ` R ) C_ ( RLReg ` R ) )
25		eqid	\|- ( 1r ` R ) = ( 1r ` R )
26	22 25	1unit	\|- ( R e. Ring -> ( 1r ` R ) e. ( Unit ` R ) )
27	22 12	unitnegcl	\|- ( ( R e. Ring /\ ( 1r ` R ) e. ( Unit ` R ) ) -> ( ( invg ` R ) ` ( 1r ` R ) ) e. ( Unit ` R ) )
28	3 26 27	syl2anc2	\|- ( ph -> ( ( invg ` R ) ` ( 1r ` R ) ) e. ( Unit ` R ) )
29	24 28	sseldd	\|- ( ph -> ( ( invg ` R ) ` ( 1r ` R ) ) e. ( RLReg ` R ) )
30	21 29	eqeltrd	\|- ( ph -> ( ( invg ` R ) ` ( 1r ` ( _I ` R ) ) ) e. ( RLReg ` R ) )
31	1 2 3 4 17 10 30 6	deg1vsca	\|- ( ph -> ( D ` ( ( ( invg ` R ) ` ( 1r ` ( _I ` R ) ) ) ( .s ` Y ) F ) ) = ( D ` F ) )
32	16 31	eqtr3d	\|- ( ph -> ( D ` ( N ` F ) ) = ( D ` F ) )

Metamath Proof Explorer

Theorem deg1invg

Proof