opprringb

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

		Ref	Expression
	Hypothesis	opprbas.1	$⊢ O = {opp}_{r} (R)$
	Assertion	opprringb	$⊢ R \in Ring \leftrightarrow O \in Ring$

Step	Hyp	Ref	Expression
1		opprbas.1	$⊢ O = {opp}_{r} (R)$
2	1	opprring	$⊢ R \in Ring \to O \in Ring$
3		eqid	$⊢ {opp}_{r} (O) = {opp}_{r} (O)$
4	3	opprring	$⊢ O \in Ring \to {opp}_{r} (O) \in Ring$
5		eqidd	$⊢ ⊤ \to {Base}_{R} = {Base}_{R}$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7	1 6	opprbas	$⊢ {Base}_{R} = {Base}_{O}$
8	3 7	opprbas	$⊢ {Base}_{R} = {Base}_{{opp}_{r} (O)}$
9	8	a1i	$⊢ ⊤ \to {Base}_{R} = {Base}_{{opp}_{r} (O)}$
10		eqid	$⊢ +_{R} = +_{R}$
11	1 10	oppradd	$⊢ +_{R} = +_{O}$
12	3 11	oppradd	$⊢ +_{R} = +_{{opp}_{r} (O)}$
13	12	oveqi	$⊢ x +_{R} y = x +_{{opp}_{r} (O)} y$
14	13	a1i	$⊢ (⊤ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x +_{R} y = x +_{{opp}_{r} (O)} y$
15		eqid	$⊢ \cdot_{O} = \cdot_{O}$
16		eqid	$⊢ \cdot_{{opp}_{r} (O)} = \cdot_{{opp}_{r} (O)}$
17	7 15 3 16	opprmul	$⊢ x \cdot_{{opp}_{r} (O)} 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} (O)} y$
21	20	a1i	$⊢ (⊤ \land (x \in {Base}_{R} \land y \in {Base}_{R})) \to x \cdot_{R} y = x \cdot_{{opp}_{r} (O)} y$
22	5 9 14 21	ringpropd	$⊢ ⊤ \to (R \in Ring \leftrightarrow {opp}_{r} (O) \in Ring)$
23	22	mptru	$⊢ R \in Ring \leftrightarrow {opp}_{r} (O) \in Ring$
24	4 23	sylibr	$⊢ O \in Ring \to R \in Ring$
25	2 24	impbii	$⊢ R \in Ring \leftrightarrow O \in Ring$

Metamath Proof Explorer