oppgid

Description: Zero in a monoid is a symmetric notion. (Contributed by Stefan O'Rear, 26-Aug-2015) (Revised by Mario Carneiro, 16-Sep-2015)

	Ref	Expression
Hypotheses	oppgbas.1	$⊢ O = {opp}_{𝑔} (R)$
	oppgid.2	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	oppgid	$⊢ \underset{˙}{0} = 0_{O}$

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	$⊢ O = {opp}_{𝑔} (R)$
2		oppgid.2	$⊢ \underset{˙}{0} = 0_{R}$
3		ancom	$⊢ (x +_{R} y = y \land y +_{R} x = y) \leftrightarrow (y +_{R} x = y \land x +_{R} y = y)$
4		eqid	$⊢ +_{R} = +_{R}$
5		eqid	$⊢ +_{O} = +_{O}$
6	4 1 5	oppgplus	$⊢ x +_{O} y = y +_{R} x$
7	6	eqeq1i	$⊢ x +_{O} y = y \leftrightarrow y +_{R} x = y$
8	4 1 5	oppgplus	$⊢ y +_{O} x = x +_{R} y$
9	8	eqeq1i	$⊢ y +_{O} x = y \leftrightarrow x +_{R} y = y$
10	7 9	anbi12i	$⊢ (x +_{O} y = y \land y +_{O} x = y) \leftrightarrow (y +_{R} x = y \land x +_{R} y = y)$
11	3 10	bitr4i	$⊢ (x +_{R} y = y \land y +_{R} x = y) \leftrightarrow (x +_{O} y = y \land y +_{O} x = y)$
12	11	ralbii	$⊢ \forall y \in {Base}_{R} (x +_{R} y = y \land y +_{R} x = y) \leftrightarrow \forall y \in {Base}_{R} (x +_{O} y = y \land y +_{O} x = y)$
13	12	anbi2i	$⊢ (x \in {Base}_{R} \land \forall y \in {Base}_{R} (x +_{R} y = y \land y +_{R} x = y)) \leftrightarrow (x \in {Base}_{R} \land \forall y \in {Base}_{R} (x +_{O} y = y \land y +_{O} x = y))$
14	13	iotabii	$⊢ (ι x \| (x \in {Base}_{R} \land \forall y \in {Base}_{R} (x +_{R} y = y \land y +_{R} x = y))) = (ι x \| (x \in {Base}_{R} \land \forall y \in {Base}_{R} (x +_{O} y = y \land y +_{O} x = y)))$
15		eqid	$⊢ {Base}_{R} = {Base}_{R}$
16	15 4 2	grpidval	$⊢ \underset{˙}{0} = (ι x \| (x \in {Base}_{R} \land \forall y \in {Base}_{R} (x +_{R} y = y \land y +_{R} x = y)))$
17	1 15	oppgbas	$⊢ {Base}_{R} = {Base}_{O}$
18		eqid	$⊢ 0_{O} = 0_{O}$
19	17 5 18	grpidval	$⊢ 0_{O} = (ι x \| (x \in {Base}_{R} \land \forall y \in {Base}_{R} (x +_{O} y = y \land y +_{O} x = y)))$
20	14 16 19	3eqtr4i	$⊢ \underset{˙}{0} = 0_{O}$

Metamath Proof Explorer

Theorem oppgid

Proof