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 ⊢ 𝑂 = ( 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 ‘ 𝑂 )