Theorem opprneg

Description: The negative function in an opposite ring. (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015)

	Ref	Expression
Hypotheses	opprbas.1	$$⊢O={opp}_r\left(R\right)$$
	opprneg.2	$$⊢N={inv}_g\left(R\right)$$
Assertion	opprneg	$$⊢N={inv}_g\left(O\right)$$

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	$$⊢O={opp}_r\left(R\right)$$
2		opprneg.2	$$⊢N={inv}_g\left(R\right)$$
3		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
4		eqid	$$⊢{+}_R={+}_R$$
5		eqid	$$⊢0_R=0_R$$
6	3 4 5 2	grpinvfval	$$⊢N=\left(x\in {\mathrm{Base}}_R⟼\left(\iota y\in {\mathrm{Base}}_R|y{+}_{R}x=0_R\right)\right)$$
7	1 3	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_O$$
8	1 4	oppradd	$$⊢{+}_R={+}_O$$
9	1 5	oppr0	$$⊢0_R=0_O$$
10		eqid	$$⊢{inv}_g\left(O\right)={inv}_g\left(O\right)$$
11	7 8 9 10	grpinvfval	$$⊢{inv}_g\left(O\right)=\left(x\in {\mathrm{Base}}_R⟼\left(\iota y\in {\mathrm{Base}}_R|y{+}_{R}x=0_R\right)\right)$$
12	6 11	eqtr4i	$$⊢N={inv}_g\left(O\right)$$