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 = opp r R
Assertion opprring R Ring O Ring

Proof

Step Hyp Ref Expression
1 opprbas.1 O = opp r 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 = 1 R z O x = 1 R O x
6 5 eqeq1d z = 1 R z O x = x 1 R O x = x
7 6 ovanraleqv z = 1 R x Base R z O x = x x O z = x x Base R 1 R O x = x x O 1 R = x
8 eqid Base R = Base R
9 eqid 1 R = 1 R
10 8 9 ringidcl R Ring 1 R Base R
11 eqid R = R
12 eqid O = O
13 8 11 1 12 opprmul 1 R O x = x R 1 R
14 8 11 9 ringridm R Ring x Base R x R 1 R = x
15 13 14 eqtrid R Ring x Base R 1 R O x = x
16 8 11 1 12 opprmul x O 1 R = 1 R R x
17 8 11 9 ringlidm R Ring x Base R 1 R R x = x
18 16 17 eqtrid R Ring x Base R x O 1 R = x
19 15 18 jca R Ring x Base R 1 R O x = x x O 1 R = x
20 19 ralrimiva R Ring x Base R 1 R O x = x x O 1 R = x
21 7 10 20 rspcedvdw R Ring z Base R x Base R z O x = x x O z = x
22 1 8 opprbas Base R = Base O
23 22 12 isringrng O Ring O Rng z Base R x Base R z O x = x x O z = x
24 4 21 23 sylanbrc R Ring O Ring