Theorem 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	⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion	opprrngb	⊢ ( 𝑅 ∈ Rng ↔ 𝑂 ∈ Rng )

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	⊢ 𝑂 = ( oppr ‘ 𝑅 )
2	1	opprrng	⊢ ( 𝑅 ∈ Rng → 𝑂 ∈ Rng )
3		eqid	⊢ ( oppr ‘ 𝑂 ) = ( oppr ‘ 𝑂 )
4	3	opprrng	⊢ ( 𝑂 ∈ Rng → ( oppr ‘ 𝑂 ) ∈ Rng )
5		eqidd	⊢ ( ⊤ → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) )
6		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7	1 6	opprbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
8	3 7	opprbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑂 ) )
9	8	a1i	⊢ ( ⊤ → ( Base ‘ 𝑅 ) = ( Base ‘ ( oppr ‘ 𝑂 ) ) )
10		eqid	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
11	1 10	oppradd	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 )
12	3 11	oppradd	⊢ ( +g ‘ 𝑅 ) = ( +g ‘ ( oppr ‘ 𝑂 ) )
13	12	oveqi	⊢ ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( oppr ‘ 𝑂 ) ) 𝑦 )
14	13	a1i	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( +g ‘ ( oppr ‘ 𝑂 ) ) 𝑦 ) )
15		eqid	⊢ ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 )
16		eqid	⊢ ( .r ‘ ( oppr ‘ 𝑂 ) ) = ( .r ‘ ( oppr ‘ 𝑂 ) )
17	7 15 3 16	opprmul	⊢ ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 )
18		eqid	⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
19	6 18 1 15	opprmul	⊢ ( 𝑦 ( .r ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 )
20	17 19	eqtr2i	⊢ ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑦 )
21	20	a1i	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( 𝑥 ( .r ‘ ( oppr ‘ 𝑂 ) ) 𝑦 ) )
22	5 9 14 21	rngpropd	⊢ ( ⊤ → ( 𝑅 ∈ Rng ↔ ( oppr ‘ 𝑂 ) ∈ Rng ) )
23	22	mptru	⊢ ( 𝑅 ∈ Rng ↔ ( oppr ‘ 𝑂 ) ∈ Rng )
24	4 23	sylibr	⊢ ( 𝑂 ∈ Rng → 𝑅 ∈ Rng )
25	2 24	impbii	⊢ ( 𝑅 ∈ Rng ↔ 𝑂 ∈ Rng )