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 = {Poly}_{1} (R)$
	deg1addle.d	$⊢ D = \deg_{1} (R)$
	deg1addle.r	$⊢ φ \to R \in Ring$
	deg1invg.b	$⊢ B = {Base}_{Y}$
	deg1invg.n	$⊢ N = {inv}_{g} (Y)$
	deg1invg.f	$⊢ φ \to F \in B$
Assertion	deg1invg	$⊢ φ \to D (N (F)) = D (F)$

Proof

Step	Hyp	Ref	Expression
1		deg1addle.y	$⊢ Y = {Poly}_{1} (R)$
2		deg1addle.d	$⊢ D = \deg_{1} (R)$
3		deg1addle.r	$⊢ φ \to R \in Ring$
4		deg1invg.b	$⊢ B = {Base}_{Y}$
5		deg1invg.n	$⊢ N = {inv}_{g} (Y)$
6		deg1invg.f	$⊢ φ \to F \in B$
7	1	ply1lmod	$⊢ R \in Ring \to Y \in LMod$
8	3 7	syl	$⊢ φ \to Y \in LMod$
9	1	ply1sca2	$⊢ I (R) = Scalar (Y)$
10		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
11		eqid	$⊢ 1_{I (R)} = 1_{I (R)}$
12		eqid	$⊢ {inv}_{g} (R) = {inv}_{g} (R)$
13	12	grpinvfvi	$⊢ {inv}_{g} (R) = {inv}_{g} (I (R))$
14	4 5 9 10 11 13	lmodvneg1	$⊢ (Y \in LMod \land F \in B) \to {inv}_{g} (R) (1_{I (R)}) \cdot_{Y} F = N (F)$
15	8 6 14	syl2anc	$⊢ φ \to {inv}_{g} (R) (1_{I (R)}) \cdot_{Y} F = N (F)$
16	15	fveq2d	$⊢ φ \to D ({inv}_{g} (R) (1_{I (R)}) \cdot_{Y} F) = D (N (F))$
17		eqid	$⊢ RLReg (R) = RLReg (R)$
18		fvi	$⊢ R \in Ring \to I (R) = R$
19	3 18	syl	$⊢ φ \to I (R) = R$
20	19	fveq2d	$⊢ φ \to 1_{I (R)} = 1_{R}$
21	20	fveq2d	$⊢ φ \to {inv}_{g} (R) (1_{I (R)}) = {inv}_{g} (R) (1_{R})$
22		eqid	$⊢ Unit (R) = Unit (R)$
23	17 22	unitrrg	$⊢ R \in Ring \to Unit (R) \subseteq RLReg (R)$
24	3 23	syl	$⊢ φ \to Unit (R) \subseteq RLReg (R)$
25		eqid	$⊢ 1_{R} = 1_{R}$
26	22 25	1unit	$⊢ R \in Ring \to 1_{R} \in Unit (R)$
27	22 12	unitnegcl	$⊢ (R \in Ring \land 1_{R} \in Unit (R)) \to {inv}_{g} (R) (1_{R}) \in Unit (R)$
28	3 26 27	syl2anc2	$⊢ φ \to {inv}_{g} (R) (1_{R}) \in Unit (R)$
29	24 28	sseldd	$⊢ φ \to {inv}_{g} (R) (1_{R}) \in RLReg (R)$
30	21 29	eqeltrd	$⊢ φ \to {inv}_{g} (R) (1_{I (R)}) \in RLReg (R)$
31	1 2 3 4 17 10 30 6	deg1vsca	$⊢ φ \to D ({inv}_{g} (R) (1_{I (R)}) \cdot_{Y} F) = D (F)$
32	16 31	eqtr3d	$⊢ φ \to D (N (F)) = D (F)$

Metamath Proof Explorer

Theorem deg1invg

Proof