Theorem opprringb

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

	Ref	Expression
Hypothesis	opprbas.1	⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion	opprringb	⊢ ( 𝑅 ∈ Ring ↔ 𝑂 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		opprbas.1	⊢ 𝑂 = ( oppr ‘ 𝑅 )
2	1	opprring	⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Ring )
3		eqid	⊢ ( oppr ‘ 𝑂 ) = ( oppr ‘ 𝑂 )
4	3	opprring	⊢ ( 𝑂 ∈ Ring → ( oppr ‘ 𝑂 ) ∈ Ring )
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	ringpropd	⊢ ( ⊤ → ( 𝑅 ∈ Ring ↔ ( oppr ‘ 𝑂 ) ∈ Ring ) )
23	22	mptru	⊢ ( 𝑅 ∈ Ring ↔ ( oppr ‘ 𝑂 ) ∈ Ring )
24	4 23	sylibr	⊢ ( 𝑂 ∈ Ring → 𝑅 ∈ Ring )
25	2 24	impbii	⊢ ( 𝑅 ∈ Ring ↔ 𝑂 ∈ Ring )