Metamath Proof Explorer

Theorem opprring

Description: An opposite ring is a ring. (Contributed by Mario Carneiro, 1-Dec-2014) (Revised by Mario Carneiro, 30-Aug-2015) (Proof shortened by AV, 30-Mar-2025)

Ref Expression
Hypothesis opprbas.1 ⊢O=oppr⁡R
Assertion opprring ⊢R∈Ring→O∈Ring

Proof

Step Hyp Ref Expression
1 opprbas.1 ⊢O=oppr⁡R
2 ringrng ⊢R∈Ring→R∈Rng
3 1 opprrng ⊢R∈Rng→O∈Rng
4 2 3 syl ⊢R∈Ring→O∈Rng
5 oveq1 ⊢z=1R→z⋅Ox=1R⋅Ox
6 5 eqeq1d ⊢z=1R→z⋅Ox=x↔1R⋅Ox=x
7 6 ovanraleqv ⊢z=1R→∀x∈BaseRz⋅Ox=x∧x⋅Oz=x↔∀x∈BaseR1R⋅Ox=x∧x⋅O1R=x
8 eqid ⊢BaseR=BaseR
9 eqid ⊢1R=1R
10 8 9 ringidcl ⊢R∈Ring→1R∈BaseR
11 eqid ⊢⋅R=⋅R
12 eqid ⊢⋅O=⋅O
13 8 11 1 12 opprmul ⊢1R⋅Ox=x⋅R1R
14 8 11 9 ringridm ⊢R∈Ring∧x∈BaseR→x⋅R1R=x
15 13 14 eqtrid ⊢R∈Ring∧x∈BaseR→1R⋅Ox=x
16 8 11 1 12 opprmul ⊢x⋅O1R=1R⋅Rx
17 8 11 9 ringlidm ⊢R∈Ring∧x∈BaseR→1R⋅Rx=x
18 16 17 eqtrid ⊢R∈Ring∧x∈BaseR→x⋅O1R=x
19 15 18 jca ⊢R∈Ring∧x∈BaseR→1R⋅Ox=x∧x⋅O1R=x
20 19 ralrimiva ⊢R∈Ring→∀x∈BaseR1R⋅Ox=x∧x⋅O1R=x
21 7 10 20 rspcedvdw ⊢R∈Ring→∃z∈BaseR∀x∈BaseRz⋅Ox=x∧x⋅Oz=x
22 1 8 opprbas ⊢BaseR=BaseO
23 22 12 isringrng ⊢O∈Ring↔O∈Rng∧∃z∈BaseR∀x∈BaseRz⋅Ox=x∧x⋅Oz=x
24 4 21 23 sylanbrc ⊢R∈Ring→O∈Ring