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 𝑂 = ( oppr𝑅 )
opprneg.2 𝑁 = ( invg𝑅 )
Assertion opprneg 𝑁 = ( invg𝑂 )

Proof

Step Hyp Ref Expression
1 opprbas.1 𝑂 = ( oppr𝑅 )
2 opprneg.2 𝑁 = ( invg𝑅 )
3 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
4 eqid ( +g𝑅 ) = ( +g𝑅 )
5 eqid ( 0g𝑅 ) = ( 0g𝑅 )
6 3 4 5 2 grpinvfval 𝑁 = ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( +g𝑅 ) 𝑥 ) = ( 0g𝑅 ) ) )
7 1 3 opprbas ( Base ‘ 𝑅 ) = ( Base ‘ 𝑂 )
8 1 4 oppradd ( +g𝑅 ) = ( +g𝑂 )
9 1 5 oppr0 ( 0g𝑅 ) = ( 0g𝑂 )
10 eqid ( invg𝑂 ) = ( invg𝑂 )
11 7 8 9 10 grpinvfval ( invg𝑂 ) = ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ ( 𝑦 ∈ ( Base ‘ 𝑅 ) ( 𝑦 ( +g𝑅 ) 𝑥 ) = ( 0g𝑅 ) ) )
12 6 11 eqtr4i 𝑁 = ( invg𝑂 )