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)

Ref Expression
Hypothesis opprbas.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
Assertion opprring ( 𝑅 ∈ Ring → 𝑂 ∈ Ring )

Proof

Step Hyp Ref Expression
1 opprbas.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 1 2 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
4 3 a1i ⊢ ( 𝑅 ∈ Ring → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 ) )
5 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
6 1 5 oppradd ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 )
7 6 a1i ⊢ ( 𝑅 ∈ Ring → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 ) )
8 eqidd ⊢ ( 𝑅 ∈ Ring → ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 ) )
9 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
10 3 6 grpprop ⊢ ( 𝑅 ∈ Grp ↔ 𝑂 ∈ Grp )
11 9 10 sylib ⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Grp )
12 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13 eqid ⊢ ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 )
14 2 12 1 13 opprmul ⊢ ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 )
15 2 12 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
16 15 3com23 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
17 14 16 eqeltrid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
18 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑅 ∈ Ring )
19 simpr3 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
20 simpr2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
21 simpr1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
22 2 12 ringass ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝑧 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) )
23 18 19 20 21 22 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝑧 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) )
24 23 eqcomd ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑧 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) = ( ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑥 ) )
25 14 oveq1i ⊢ ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) ( .r ‘ 𝑂 ) 𝑧 ) = ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑂 ) 𝑧 )
26 2 12 1 13 opprmul ⊢ ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ( .r ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
27 25 26 eqtri ⊢ ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) ( .r ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) )
28 2 12 1 13 opprmul ⊢ ( 𝑦 ( .r ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 )
29 28 oveq2i ⊢ ( 𝑥 ( .r ‘ 𝑂 ) ( 𝑦 ( .r ‘ 𝑂 ) 𝑧 ) ) = ( 𝑥 ( .r ‘ 𝑂 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) )
30 2 12 1 13 opprmul ⊢ ( 𝑥 ( .r ‘ 𝑂 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑥 )
31 29 30 eqtri ⊢ ( 𝑥 ( .r ‘ 𝑂 ) ( 𝑦 ( .r ‘ 𝑂 ) 𝑧 ) ) = ( ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑥 )
32 24 27 31 3eqtr4g ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) ( .r ‘ 𝑂 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑂 ) ( 𝑦 ( .r ‘ 𝑂 ) 𝑧 ) ) )
33 2 5 12 ringdir ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) ) )
34 18 20 19 21 33 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) ) )
35 2 12 1 13 opprmul ⊢ ( 𝑥 ( .r ‘ 𝑂 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ( .r ‘ 𝑅 ) 𝑥 )
36 2 12 1 13 opprmul ⊢ ( 𝑥 ( .r ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 )
37 14 36 oveq12i ⊢ ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑂 ) 𝑧 ) ) = ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) )
38 34 35 37 3eqtr4g ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( .r ‘ 𝑂 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑂 ) 𝑧 ) ) )
39 2 5 12 ringdi ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑧 ( .r ‘ 𝑅 ) ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) )
40 18 19 21 20 39 syl13anc ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑧 ( .r ‘ 𝑅 ) ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) )
41 2 12 1 13 opprmul ⊢ ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑂 ) 𝑧 ) = ( 𝑧 ( .r ‘ 𝑅 ) ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) )
42 36 28 oveq12i ⊢ ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑂 ) 𝑧 ) ) = ( ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) )
43 40 41 42 3eqtr4g ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑂 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑂 ) 𝑧 ) ) )
44 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
45 2 44 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
46 2 12 1 13 opprmul ⊢ ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑂 ) 𝑥 ) = ( 𝑥 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
47 2 12 44 ringridm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 𝑥 )
48 46 47 syl5eq ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑂 ) 𝑥 ) = 𝑥 )
49 2 12 1 13 opprmul ⊢ ( 𝑥 ( .r ‘ 𝑂 ) ( 1r ‘ 𝑅 ) ) = ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 )
50 2 12 44 ringlidm ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( ( 1r ‘ 𝑅 ) ( .r ‘ 𝑅 ) 𝑥 ) = 𝑥 )
51 49 50 syl5eq ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑂 ) ( 1r ‘ 𝑅 ) ) = 𝑥 )
52 4 7 8 11 17 32 38 43 45 48 51 isringd ⊢ ( 𝑅 ∈ Ring → 𝑂 ∈ Ring )