Theorem ringnegl

Description: Negation in a ring is the same as left multiplication by -1. ( rngonegmn1l analog.) (Contributed by Jeff Madsen, 19-Jun-2010) (Revised by Mario Carneiro, 2-Jul-2014)

	Ref	Expression
Hypotheses	ringnegl.b	$$⊢B={\mathrm{Base}}_R$$
	ringnegl.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
	ringnegl.u	$$⊢\underset{\dot{}}{1}=1_R$$
	ringnegl.n	$$⊢N={inv}_g\left(R\right)$$
	ringnegl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
	ringnegl.x	$$⊢\phi \to X\in B$$
Assertion	ringnegl	$$⊢\phi \to N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X=N\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		ringnegl.b	$$⊢B={\mathrm{Base}}_R$$
2		ringnegl.t	$$⊢\underset{\dot{}}{·}={\cdot }_R$$
3		ringnegl.u	$$⊢\underset{\dot{}}{1}=1_R$$
4		ringnegl.n	$$⊢N={inv}_g\left(R\right)$$
5		ringnegl.r	$$⊢\phi \to R\in \mathrm{Ring}$$
6		ringnegl.x	$$⊢\phi \to X\in B$$
7	1 3	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
8	5 7	syl	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
9		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
10	5 9	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
11	1 4	grpinvcl	$$⊢\left(R\in \mathrm{Grp}\wedge \underset{\dot{}}{1}\in B\right)\to N\left(\underset{\dot{}}{1}\right)\in B$$
12	10 8 11	syl2anc	$$⊢\phi \to N\left(\underset{\dot{}}{1}\right)\in B$$
13		eqid	$$⊢{+}_R={+}_R$$
14	1 13 2	ringdir	$$⊢\left(R\in \mathrm{Ring}\wedge \left(\underset{\dot{}}{1}\in B\wedge N\left(\underset{\dot{}}{1}\right)\in B\wedge X\in B\right)\right)\to \left(\underset{\dot{}}{1}{+}_{R}N\left(\underset{\dot{}}{1}\right)\right)\underset{\dot{}}{·}X=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right){+}_R\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)$$
15	5 8 12 6 14	syl13anc	$$⊢\phi \to \left(\underset{\dot{}}{1}{+}_{R}N\left(\underset{\dot{}}{1}\right)\right)\underset{\dot{}}{·}X=\left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right){+}_R\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)$$
16		eqid	$$⊢0_R=0_R$$
17	1 13 16 4	grprinv	$$⊢\left(R\in \mathrm{Grp}\wedge \underset{\dot{}}{1}\in B\right)\to \underset{\dot{}}{1}{+}_{R}N\left(\underset{\dot{}}{1}\right)=0_R$$
18	10 8 17	syl2anc	$$⊢\phi \to \underset{\dot{}}{1}{+}_{R}N\left(\underset{\dot{}}{1}\right)=0_R$$
19	18	oveq1d	$$⊢\phi \to \left(\underset{\dot{}}{1}{+}_{R}N\left(\underset{\dot{}}{1}\right)\right)\underset{\dot{}}{·}X=0_R\underset{\dot{}}{·}X$$
20	1 2 16	ringlz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to 0_R\underset{\dot{}}{·}X=0_R$$
21	5 6 20	syl2anc	$$⊢\phi \to 0_R\underset{\dot{}}{·}X=0_R$$
22	19 21	eqtrd	$$⊢\phi \to \left(\underset{\dot{}}{1}{+}_{R}N\left(\underset{\dot{}}{1}\right)\right)\underset{\dot{}}{·}X=0_R$$
23	1 2 3	ringlidm	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$
24	5 6 23	syl2anc	$$⊢\phi \to \underset{\dot{}}{1}\underset{\dot{}}{·}X=X$$
25	24	oveq1d	$$⊢\phi \to \left(\underset{\dot{}}{1}\underset{\dot{}}{·}X\right){+}_R\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)=X{+}_R\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)$$
26	15 22 25	3eqtr3rd	$$⊢\phi \to X{+}_R\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)=0_R$$
27	1 2	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge N\left(\underset{\dot{}}{1}\right)\in B\wedge X\in B\right)\to N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\in B$$
28	5 12 6 27	syl3anc	$$⊢\phi \to N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\in B$$
29	1 13 16 4	grpinvid1	$$⊢\left(R\in \mathrm{Grp}\wedge X\in B\wedge N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\in B\right)\to \left(N\left(X\right)=N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\leftrightarrow X{+}_R\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)=0_R\right)$$
30	10 6 28 29	syl3anc	$$⊢\phi \to \left(N\left(X\right)=N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\leftrightarrow X{+}_R\left(N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X\right)=0_R\right)$$
31	26 30	mpbird	$$⊢\phi \to N\left(X\right)=N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X$$
32	31	eqcomd	$$⊢\phi \to N\left(\underset{\dot{}}{1}\right)\underset{\dot{}}{·}X=N\left(X\right)$$