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

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