Theorem ringnegr

Description: Negation in a ring is the same as right multiplication by -1. ( rngonegmn1r 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	ringnegr	$$⊢\phi \to X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)=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		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
8	5 7	syl	$$⊢\phi \to R\in \mathrm{Grp}$$
9	1 3	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in B$$
10	5 9	syl	$$⊢\phi \to \underset{\dot{}}{1}\in B$$
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	8 10 11	syl2anc	$$⊢\phi \to N\left(\underset{\dot{}}{1}\right)\in B$$
13		eqid	$$⊢{+}_R={+}_R$$
14	1 13 2	ringdi	$$⊢\left(R\in \mathrm{Ring}\wedge \left(X\in B\wedge N\left(\underset{\dot{}}{1}\right)\in B\wedge \underset{\dot{}}{1}\in B\right)\right)\to X\underset{\dot{}}{·}\left(N\left(\underset{\dot{}}{1}\right){+}_R\underset{\dot{}}{1}\right)=\left(X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)\right){+}_R\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
15	5 6 12 10 14	syl13anc	$$⊢\phi \to X\underset{\dot{}}{·}\left(N\left(\underset{\dot{}}{1}\right){+}_R\underset{\dot{}}{1}\right)=\left(X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)\right){+}_R\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
16		eqid	$$⊢0_R=0_R$$
17	1 13 16 4	grplinv	$$⊢\left(R\in \mathrm{Grp}\wedge \underset{\dot{}}{1}\in B\right)\to N\left(\underset{\dot{}}{1}\right){+}_R\underset{\dot{}}{1}=0_R$$
18	8 10 17	syl2anc	$$⊢\phi \to N\left(\underset{\dot{}}{1}\right){+}_R\underset{\dot{}}{1}=0_R$$
19	18	oveq2d	$$⊢\phi \to X\underset{\dot{}}{·}\left(N\left(\underset{\dot{}}{1}\right){+}_R\underset{\dot{}}{1}\right)=X\underset{\dot{}}{·}{0}_R$$
20	1 2 16	ringrz	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{·}{0}_R=0_R$$
21	5 6 20	syl2anc	$$⊢\phi \to X\underset{\dot{}}{·}{0}_R=0_R$$
22	19 21	eqtrd	$$⊢\phi \to X\underset{\dot{}}{·}\left(N\left(\underset{\dot{}}{1}\right){+}_R\underset{\dot{}}{1}\right)=0_R$$
23	1 2 3	ringridm	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\right)\to X\underset{\dot{}}{·}\underset{\dot{}}{1}=X$$
24	5 6 23	syl2anc	$$⊢\phi \to X\underset{\dot{}}{·}\underset{\dot{}}{1}=X$$
25	24	oveq2d	$$⊢\phi \to \left(X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)\right){+}_R\left(X\underset{\dot{}}{·}\underset{\dot{}}{1}\right)=\left(X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)\right){+}_{R}X$$
26	15 22 25	3eqtr3rd	$$⊢\phi \to \left(X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)\right){+}_{R}X=0_R$$
27	1 2	ringcl	$$⊢\left(R\in \mathrm{Ring}\wedge X\in B\wedge N\left(\underset{\dot{}}{1}\right)\in B\right)\to X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)\in B$$
28	5 6 12 27	syl3anc	$$⊢\phi \to X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)\in B$$
29	1 13 16 4	grpinvid2	$$⊢\left(R\in \mathrm{Grp}\wedge X\in B\wedge X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)\in B\right)\to \left(N\left(X\right)=X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)\leftrightarrow \left(X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)\right){+}_{R}X=0_R\right)$$
30	8 6 28 29	syl3anc	$$⊢\phi \to \left(N\left(X\right)=X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)\leftrightarrow \left(X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)\right){+}_{R}X=0_R\right)$$
31	26 30	mpbird	$$⊢\phi \to N\left(X\right)=X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)$$
32	31	eqcomd	$$⊢\phi \to X\underset{\dot{}}{·}N\left(\underset{\dot{}}{1}\right)=N\left(X\right)$$