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 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion opprring ( 𝑅 ∈ Ring → 𝑂 ∈ Ring )

Proof

Step Hyp Ref Expression
1 opprbas.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 ringrng ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
3 1 opprrng ⊢ ( 𝑅 ∈ Rng → 𝑂 ∈ Rng )
4 2 3 syl ⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Rng )
5 oveq1 ⊢ ( 𝑧 = ( 1r ‘ 𝑅 ) → ( 𝑧 ( .r ‘ 𝑂 ) 𝑥 ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑂 ) 𝑥 ) )
6 5 eqeq1d ⊢ ( 𝑧 = ( 1r ‘ 𝑅 ) → ( ( 𝑧 ( .r ‘ 𝑂 ) 𝑥 ) = 𝑥 ↔ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑂 ) 𝑥 ) = 𝑥 ) )
7 6 ovanraleqv ⊢ ( 𝑧 = ( 1r ‘ 𝑅 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑧 ( .r ‘ 𝑂 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑂 ) 𝑧 ) = 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑂 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑂 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) ) )
8 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
9 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
10 8 9 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
11 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
12 eqid ⊢ ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 )
13 8 11 1 12 opprmul ⊢ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
14 8 11 9 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑥 )
15 13 14 eqtrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑂 ) 𝑥 ) = 𝑥 )
16 8 11 1 12 opprmul ⊢ ( 𝑥 ( .r ‘ 𝑂 ) ( 1r ‘ 𝑅 ) ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 )
17 8 11 9 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
18 16 17 eqtrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑂 ) ( 1r ‘ 𝑅 ) ) = 𝑥 )
19 15 18 jca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑂 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑂 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) )
20 19 ralrimiva ⊢ ( 𝑅 ∈ Ring → ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑂 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑂 ) ( 1r ‘ 𝑅 ) ) = 𝑥 ) )
21 7 10 20 rspcedvdw ⊢ ( 𝑅 ∈ Ring → ∃ 𝑧 ∈ ( Base ‘ 𝑅 ) ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑧 ( .r ‘ 𝑂 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑂 ) 𝑧 ) = 𝑥 ) )
22 1 8 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
23 22 12 isringrng ⊢ ( 𝑂 ∈ Ring ↔ ( 𝑂 ∈ Rng ∧ ∃ 𝑧 ∈ ( Base ‘ 𝑅 ) ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ( ( 𝑧 ( .r ‘ 𝑂 ) 𝑥 ) = 𝑥 ∧ ( 𝑥 ( .r ‘ 𝑂 ) 𝑧 ) = 𝑥 ) ) )
24 4 21 23 sylanbrc ⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Ring )