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 )