Theorem opprringb

Description: Bidirectional form of opprring . (Contributed by Mario Carneiro, 6-Dec-2014)

	Ref	Expression
Hypothesis	opprbas.1	$$⊢O={opp}_r\left(R\right)$$
Assertion	opprringb	$$⊢R\in \mathrm{Ring}\leftrightarrow O\in \mathrm{Ring}$$

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	$$⊢O={opp}_r\left(R\right)$$
2	1	opprring	$$⊢R\in \mathrm{Ring}\to O\in \mathrm{Ring}$$
3		eqid	$$⊢{opp}_r\left(O\right)={opp}_r\left(O\right)$$
4	3	opprring	$$⊢O\in \mathrm{Ring}\to {opp}_r\left(O\right)\in \mathrm{Ring}$$
5		eqidd	$$⊢\top \to {\mathrm{Base}}_R={\mathrm{Base}}_R$$
6		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
7	1 6	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_O$$
8	3 7	opprbas	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_{{opp}_r\left(O\right)}$$
9	8	a1i	$$⊢\top \to {\mathrm{Base}}_R={\mathrm{Base}}_{{opp}_r\left(O\right)}$$
10		eqid	$$⊢{+}_R={+}_R$$
11	1 10	oppradd	$$⊢{+}_R={+}_O$$
12	3 11	oppradd	$$⊢{+}_R={+}_{{opp}_r\left(O\right)}$$
13	12	oveqi	$$⊢x{+}_{R}y=x{+}_{{opp}_r\left(O\right)}y$$
14	13	a1i	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to x{+}_{R}y=x{+}_{{opp}_r\left(O\right)}y$$
15		eqid	$$⊢{\cdot }_O={\cdot }_O$$
16		eqid	$$⊢{\cdot }_{{opp}_r\left(O\right)}={\cdot }_{{opp}_r\left(O\right)}$$
17	7 15 3 16	opprmul	$$⊢x{\cdot }_{{opp}_r\left(O\right)}y=y{\cdot }_{O}x$$
18		eqid	$$⊢{\cdot }_R={\cdot }_R$$
19	6 18 1 15	opprmul	$$⊢y{\cdot }_{O}x=x{\cdot }_{R}y$$
20	17 19	eqtr2i	$$⊢x{\cdot }_{R}y=x{\cdot }_{{opp}_r\left(O\right)}y$$
21	20	a1i	$$⊢\left(\top \wedge \left(x\in {\mathrm{Base}}_R\wedge y\in {\mathrm{Base}}_R\right)\right)\to x{\cdot }_{R}y=x{\cdot }_{{opp}_r\left(O\right)}y$$
22	5 9 14 21	ringpropd	$$⊢\top \to \left(R\in \mathrm{Ring}\leftrightarrow {opp}_r\left(O\right)\in \mathrm{Ring}\right)$$
23	22	mptru	$$⊢R\in \mathrm{Ring}\leftrightarrow {opp}_r\left(O\right)\in \mathrm{Ring}$$
24	4 23	sylibr	$$⊢O\in \mathrm{Ring}\to R\in \mathrm{Ring}$$
25	2 24	impbii	$$⊢R\in \mathrm{Ring}\leftrightarrow O\in \mathrm{Ring}$$