This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )