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

Metamath Proof Explorer

Theorem opprneg

Description: The negative function in an opposite ring. (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by Mario Carneiro, 2-Oct-2015)

Ref Expression
Hypotheses opprbas.1 ⊢ O = opp r ⁡ R
opprneg.2 ⊢ N = inv g ⁡ R
Assertion opprneg ⊢ N = inv g ⁡ O

Proof

Step Hyp Ref Expression
1 opprbas.1 ⊢ O = opp r ⁡ R
2 opprneg.2 ⊢ N = inv g ⁡ R
3 eqid ⊢ Base R = Base R
4 eqid ⊢ + R = + R
5 eqid ⊢ 0 R = 0 R
6 3 4 5 2 grpinvfval ⊢ N = x ∈ Base R ⟼ ι y ∈ Base R | y + R x = 0 R
7 1 3 opprbas ⊢ Base R = Base O
8 1 4 oppradd ⊢ + R = + O
9 1 5 oppr0 ⊢ 0 R = 0 O
10 eqid ⊢ inv g ⁡ O = inv g ⁡ O
11 7 8 9 10 grpinvfval ⊢ inv g ⁡ O = x ∈ Base R ⟼ ι y ∈ Base R | y + R x = 0 R
12 6 11 eqtr4i ⊢ N = inv g ⁡ O