Theorem 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	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
	deg1addle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
	deg1addle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	deg1invg.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
	deg1invg.n	⊢ 𝑁 = ( invg ‘ 𝑌 )
	deg1invg.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	deg1invg	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑁 ‘ 𝐹 ) ) = ( 𝐷 ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	⊢ 𝑌 = ( Poly1 ‘ 𝑅 )
2		deg1addle.d	⊢ 𝐷 = ( deg1 ‘ 𝑅 )
3		deg1addle.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
4		deg1invg.b	⊢ 𝐵 = ( Base ‘ 𝑌 )
5		deg1invg.n	⊢ 𝑁 = ( invg ‘ 𝑌 )
6		deg1invg.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
7	1	ply1lmod	⊢ ( 𝑅 ∈ Ring → 𝑌 ∈ LMod )
8	3 7	syl	⊢ ( 𝜑 → 𝑌 ∈ LMod )
9	1	ply1sca2	⊢ ( I ‘ 𝑅 ) = ( Scalar ‘ 𝑌 )
10		eqid	⊢ ( ·𝑠 ‘ 𝑌 ) = ( ·𝑠 ‘ 𝑌 )
11		eqid	⊢ ( 1r ‘ ( I ‘ 𝑅 ) ) = ( 1r ‘ ( I ‘ 𝑅 ) )
12		eqid	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
13	12	grpinvfvi	⊢ ( invg ‘ 𝑅 ) = ( invg ‘ ( I ‘ 𝑅 ) )
14	4 5 9 10 11 13	lmodvneg1	⊢ ( ( 𝑌 ∈ LMod ∧ 𝐹 ∈ 𝐵 ) → ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ ( I ‘ 𝑅 ) ) ) ( ·𝑠 ‘ 𝑌 ) 𝐹 ) = ( 𝑁 ‘ 𝐹 ) )
15	8 6 14	syl2anc	⊢ ( 𝜑 → ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ ( I ‘ 𝑅 ) ) ) ( ·𝑠 ‘ 𝑌 ) 𝐹 ) = ( 𝑁 ‘ 𝐹 ) )
16	15	fveq2d	⊢ ( 𝜑 → ( 𝐷 ‘ ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ ( I ‘ 𝑅 ) ) ) ( ·𝑠 ‘ 𝑌 ) 𝐹 ) ) = ( 𝐷 ‘ ( 𝑁 ‘ 𝐹 ) ) )
17		eqid	⊢ ( RLReg ‘ 𝑅 ) = ( RLReg ‘ 𝑅 )
18		fvi	⊢ ( 𝑅 ∈ Ring → ( I ‘ 𝑅 ) = 𝑅 )
19	3 18	syl	⊢ ( 𝜑 → ( I ‘ 𝑅 ) = 𝑅 )
20	19	fveq2d	⊢ ( 𝜑 → ( 1r ‘ ( I ‘ 𝑅 ) ) = ( 1r ‘ 𝑅 ) )
21	20	fveq2d	⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ ( I ‘ 𝑅 ) ) ) = ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) )
22		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
23	17 22	unitrrg	⊢ ( 𝑅 ∈ Ring → ( Unit ‘ 𝑅 ) ⊆ ( RLReg ‘ 𝑅 ) )
24	3 23	syl	⊢ ( 𝜑 → ( Unit ‘ 𝑅 ) ⊆ ( RLReg ‘ 𝑅 ) )
25		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
26	22 25	1unit	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) )
27	22 12	unitnegcl	⊢ ( ( 𝑅 ∈ Ring ∧ ( 1r ‘ 𝑅 ) ∈ ( Unit ‘ 𝑅 ) ) → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
28	3 26 27	syl2anc2	⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( Unit ‘ 𝑅 ) )
29	24 28	sseldd	⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∈ ( RLReg ‘ 𝑅 ) )
30	21 29	eqeltrd	⊢ ( 𝜑 → ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ ( I ‘ 𝑅 ) ) ) ∈ ( RLReg ‘ 𝑅 ) )
31	1 2 3 4 17 10 30 6	deg1vsca	⊢ ( 𝜑 → ( 𝐷 ‘ ( ( ( invg ‘ 𝑅 ) ‘ ( 1r ‘ ( I ‘ 𝑅 ) ) ) ( ·𝑠 ‘ 𝑌 ) 𝐹 ) ) = ( 𝐷 ‘ 𝐹 ) )
32	16 31	eqtr3d	⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑁 ‘ 𝐹 ) ) = ( 𝐷 ‘ 𝐹 ) )