opprrngb

Description: A class is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng . (Contributed by AV, 15-Feb-2025)

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

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	$⊢ O = {opp}_{r} (R)$
2	1	opprrng	$⊢ R \in Rng \to O \in Rng$
3		eqid	$⊢ {opp}_{r} (O) = {opp}_{r} (O)$
4	3	opprrng	$⊢ O \in Rng \to {opp}_{r} (O) \in Rng$
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	rngpropd	$⊢ ⊤ \to (R \in Rng \leftrightarrow {opp}_{r} (O) \in Rng)$
23	22	mptru	$⊢ R \in Rng \leftrightarrow {opp}_{r} (O) \in Rng$
24	4 23	sylibr	$⊢ O \in Rng \to R \in Rng$
25	2 24	impbii	$⊢ R \in Rng \leftrightarrow O \in Rng$

Metamath Proof Explorer

Theorem opprrngb

Proof