oppr0

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

Step	Hyp	Ref	Expression
1		opprbas.1	$⊢ O = {opp}_{r} (R)$
2		oppr0.2	$⊢ \underset{˙}{0} = 0_{R}$
3		eqid	$⊢ {Base}_{R} = {Base}_{R}$
4		eqid	$⊢ +_{R} = +_{R}$
5	3 4 2	grpidval	$⊢ \underset{˙}{0} = (ι y \| (y \in {Base}_{R} \land \forall x \in {Base}_{R} (y +_{R} x = x \land x +_{R} y = x)))$
6	1 3	opprbas	$⊢ {Base}_{R} = {Base}_{O}$
7	1 4	oppradd	$⊢ +_{R} = +_{O}$
8		eqid	$⊢ 0_{O} = 0_{O}$
9	6 7 8	grpidval	$⊢ 0_{O} = (ι y \| (y \in {Base}_{R} \land \forall x \in {Base}_{R} (y +_{R} x = x \land x +_{R} y = x)))$
10	5 9	eqtr4i	$⊢ \underset{˙}{0} = 0_{O}$

Metamath Proof Explorer