oppgmnd

Description: The opposite of a monoid is a monoid. (Contributed by Stefan O'Rear, 26-Aug-2015) (Revised by Mario Carneiro, 16-Sep-2015)

		Ref	Expression
	Hypothesis	oppgbas.1	$⊢ O = {opp}_{𝑔} (R)$
	Assertion	oppgmnd	$⊢ R \in Mnd \to O \in Mnd$

Proof

Step	Hyp	Ref	Expression
1		oppgbas.1	$⊢ O = {opp}_{𝑔} (R)$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3	1 2	oppgbas	$⊢ {Base}_{R} = {Base}_{O}$
4	3	a1i	$⊢ R \in Mnd \to {Base}_{R} = {Base}_{O}$
5		eqidd	$⊢ R \in Mnd \to +_{O} = +_{O}$
6		eqid	$⊢ +_{R} = +_{R}$
7		eqid	$⊢ +_{O} = +_{O}$
8	6 1 7	oppgplus	$⊢ x +_{O} y = y +_{R} x$
9	2 6	mndcl	$⊢ (R \in Mnd \land y \in {Base}_{R} \land x \in {Base}_{R}) \to y +_{R} x \in {Base}_{R}$
10	9	3com23	$⊢ (R \in Mnd \land x \in {Base}_{R} \land y \in {Base}_{R}) \to y +_{R} x \in {Base}_{R}$
11	8 10	eqeltrid	$⊢ (R \in Mnd \land x \in {Base}_{R} \land y \in {Base}_{R}) \to x +_{O} y \in {Base}_{R}$
12		simpl	$⊢ (R \in Mnd \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to R \in Mnd$
13		simpr3	$⊢ (R \in Mnd \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to z \in {Base}_{R}$
14		simpr2	$⊢ (R \in Mnd \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to y \in {Base}_{R}$
15		simpr1	$⊢ (R \in Mnd \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to x \in {Base}_{R}$
16	2 6	mndass	$⊢ (R \in Mnd \land (z \in {Base}_{R} \land y \in {Base}_{R} \land x \in {Base}_{R})) \to (z +_{R} y) +_{R} x = z +_{R} (y +_{R} x)$
17	12 13 14 15 16	syl13anc	$⊢ (R \in Mnd \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (z +_{R} y) +_{R} x = z +_{R} (y +_{R} x)$
18	17	eqcomd	$⊢ (R \in Mnd \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to z +_{R} (y +_{R} x) = (z +_{R} y) +_{R} x$
19	8	oveq1i	$⊢ (x +_{O} y) +_{O} z = (y +_{R} x) +_{O} z$
20	6 1 7	oppgplus	$⊢ (y +_{R} x) +_{O} z = z +_{R} (y +_{R} x)$
21	19 20	eqtri	$⊢ (x +_{O} y) +_{O} z = z +_{R} (y +_{R} x)$
22	6 1 7	oppgplus	$⊢ y +_{O} z = z +_{R} y$
23	22	oveq2i	$⊢ x +_{O} (y +_{O} z) = x +_{O} (z +_{R} y)$
24	6 1 7	oppgplus	$⊢ x +_{O} (z +_{R} y) = (z +_{R} y) +_{R} x$
25	23 24	eqtri	$⊢ x +_{O} (y +_{O} z) = (z +_{R} y) +_{R} x$
26	18 21 25	3eqtr4g	$⊢ (R \in Mnd \land (x \in {Base}_{R} \land y \in {Base}_{R} \land z \in {Base}_{R})) \to (x +_{O} y) +_{O} z = x +_{O} (y +_{O} z)$
27		eqid	$⊢ 0_{R} = 0_{R}$
28	2 27	mndidcl	$⊢ R \in Mnd \to 0_{R} \in {Base}_{R}$
29	6 1 7	oppgplus	$⊢ 0_{R} +_{O} x = x +_{R} 0_{R}$
30	2 6 27	mndrid	$⊢ (R \in Mnd \land x \in {Base}_{R}) \to x +_{R} 0_{R} = x$
31	29 30	syl5eq	$⊢ (R \in Mnd \land x \in {Base}_{R}) \to 0_{R} +_{O} x = x$
32	6 1 7	oppgplus	$⊢ x +_{O} 0_{R} = 0_{R} +_{R} x$
33	2 6 27	mndlid	$⊢ (R \in Mnd \land x \in {Base}_{R}) \to 0_{R} +_{R} x = x$
34	32 33	syl5eq	$⊢ (R \in Mnd \land x \in {Base}_{R}) \to x +_{O} 0_{R} = x$
35	4 5 11 26 28 31 34	ismndd	$⊢ R \in Mnd \to O \in Mnd$

Metamath Proof Explorer

Theorem oppgmnd

Proof