Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑁 ‘ 𝐹 ) ) = ( 𝐷 ‘ 𝐹 ) )