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

Metamath Proof Explorer

Theorem opprrng

Description: An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 opprbas.1 ⊢ 𝑂 = ( oppr ‘ 𝑅 )
2 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 1 2 opprbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
4 3 a1i ⊢ ( 𝑅 ∈ Rng → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 ) )
5 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
6 1 5 oppradd ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 )
7 6 a1i ⊢ ( 𝑅 ∈ Rng → ( +g ‘ 𝑅 ) = ( +g ‘ 𝑂 ) )
8 eqidd ⊢ ( 𝑅 ∈ Rng → ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 ) )
9 rngabl ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Abel )
10 3 6 ablprop ⊢ ( 𝑅 ∈ Abel ↔ 𝑂 ∈ Abel )
11 9 10 sylib ⊢ ( 𝑅 ∈ Rng → 𝑂 ∈ Abel )
12 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
13 eqid ⊢ ( .r ‘ 𝑂 ) = ( .r ‘ 𝑂 )
14 2 12 1 13 opprmul ⊢ ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 )
15 2 12 rngcl ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
16 15 3com23 ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
17 14 16 eqeltrid ⊢ ( ( 𝑅 ∈ Rng ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) → ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) ∈ ( Base ‘ 𝑅 ) )
18 simpl ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑅 ∈ Rng )
19 simpr3 ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑧 ∈ ( Base ‘ 𝑅 ) )
20 simpr2 ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑅 ) )
21 simpr1 ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑅 ) )
22 2 12 rngass ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝑧 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) )
23 18 19 20 21 22 syl13anc ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( 𝑧 ( .r ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ) )
24 23 eqcomd ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( 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 ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) ( .r ‘ 𝑂 ) 𝑧 ) = ( 𝑥 ( .r ‘ 𝑂 ) ( 𝑦 ( .r ‘ 𝑂 ) 𝑧 ) ) )
33 2 5 12 rngdir ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ( .r ‘ 𝑅 ) 𝑥 ) = ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) ) )
34 18 20 19 21 33 syl13anc ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( 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 ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑥 ( .r ‘ 𝑂 ) ( 𝑦 ( +g ‘ 𝑅 ) 𝑧 ) ) = ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑦 ) ( +g ‘ 𝑅 ) ( 𝑥 ( .r ‘ 𝑂 ) 𝑧 ) ) )
39 2 5 12 rngdi ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑧 ∈ ( Base ‘ 𝑅 ) ∧ 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ) ) → ( 𝑧 ( .r ‘ 𝑅 ) ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝑧 ( .r ‘ 𝑅 ) 𝑥 ) ( +g ‘ 𝑅 ) ( 𝑧 ( .r ‘ 𝑅 ) 𝑦 ) ) )
40 18 19 21 20 39 syl13anc ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( 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 ⊢ ( ( 𝑅 ∈ Rng ∧ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ ( Base ‘ 𝑅 ) ∧ 𝑧 ∈ ( Base ‘ 𝑅 ) ) ) → ( ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ( .r ‘ 𝑂 ) 𝑧 ) = ( ( 𝑥 ( .r ‘ 𝑂 ) 𝑧 ) ( +g ‘ 𝑅 ) ( 𝑦 ( .r ‘ 𝑂 ) 𝑧 ) ) )
44 4 7 8 11 17 32 38 43 isrngd ⊢ ( 𝑅 ∈ Rng → 𝑂 ∈ Rng )