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

Metamath Proof Explorer

Theorem oppr0

Description: Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014)

Ref Expression
Hypotheses opprbas.1 
|- O = ( oppR ` R )
oppr0.2 
|- .0. = ( 0g ` R )
Assertion oppr0 
|- .0. = ( 0g ` O )

Proof

Step Hyp Ref Expression
1 opprbas.1 
 |-  O = ( oppR ` R )
2 oppr0.2 
 |-  .0. = ( 0g ` R )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 eqid 
 |-  ( +g ` R ) = ( +g ` R )
5 3 4 2 grpidval 
 |-  .0. = ( iota y ( y e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( y ( +g ` R ) x ) = x /\ ( x ( +g ` R ) y ) = x ) ) )
6 1 3 opprbas 
 |-  ( Base ` R ) = ( Base ` O )
7 1 4 oppradd 
 |-  ( +g ` R ) = ( +g ` O )
8 eqid 
 |-  ( 0g ` O ) = ( 0g ` O )
9 6 7 8 grpidval 
 |-  ( 0g ` O ) = ( iota y ( y e. ( Base ` R ) /\ A. x e. ( Base ` R ) ( ( y ( +g ` R ) x ) = x /\ ( x ( +g ` R ) y ) = x ) ) )
10 5 9 eqtr4i 
 |-  .0. = ( 0g ` O )