cntzsubm

Description: Centralizers in a monoid are submonoids. (Contributed by Stefan O'Rear, 6-Sep-2015) (Revised by Mario Carneiro, 19-Apr-2016)

	Ref	Expression
Hypotheses	cntzrec.b	$⊢ B = {Base}_{M}$
	cntzrec.z	$⊢ Z = Cntz (M)$
Assertion	cntzsubm	$⊢ (M \in Mnd \land S \subseteq B) \to Z (S) \in SubMnd (M)$

Proof

Step	Hyp	Ref	Expression
1		cntzrec.b	$⊢ B = {Base}_{M}$
2		cntzrec.z	$⊢ Z = Cntz (M)$
3	1 2	cntzssv	$⊢ Z (S) \subseteq B$
4	3	a1i	$⊢ (M \in Mnd \land S \subseteq B) \to Z (S) \subseteq B$
5		eqid	$⊢ 0_{M} = 0_{M}$
6	1 5	mndidcl	$⊢ M \in Mnd \to 0_{M} \in B$
7	6	adantr	$⊢ (M \in Mnd \land S \subseteq B) \to 0_{M} \in B$
8		simpll	$⊢ ((M \in Mnd \land S \subseteq B) \land x \in S) \to M \in Mnd$
9		simpr	$⊢ (M \in Mnd \land S \subseteq B) \to S \subseteq B$
10	9	sselda	$⊢ ((M \in Mnd \land S \subseteq B) \land x \in S) \to x \in B$
11		eqid	$⊢ +_{M} = +_{M}$
12	1 11 5	mndlid	$⊢ (M \in Mnd \land x \in B) \to 0_{M} +_{M} x = x$
13	8 10 12	syl2anc	$⊢ ((M \in Mnd \land S \subseteq B) \land x \in S) \to 0_{M} +_{M} x = x$
14	1 11 5	mndrid	$⊢ (M \in Mnd \land x \in B) \to x +_{M} 0_{M} = x$
15	8 10 14	syl2anc	$⊢ ((M \in Mnd \land S \subseteq B) \land x \in S) \to x +_{M} 0_{M} = x$
16	13 15	eqtr4d	$⊢ ((M \in Mnd \land S \subseteq B) \land x \in S) \to 0_{M} +_{M} x = x +_{M} 0_{M}$
17	16	ralrimiva	$⊢ (M \in Mnd \land S \subseteq B) \to \forall x \in S 0_{M} +_{M} x = x +_{M} 0_{M}$
18	1 11 2	elcntz	$⊢ S \subseteq B \to (0_{M} \in Z (S) \leftrightarrow (0_{M} \in B \land \forall x \in S 0_{M} +_{M} x = x +_{M} 0_{M}))$
19	18	adantl	$⊢ (M \in Mnd \land S \subseteq B) \to (0_{M} \in Z (S) \leftrightarrow (0_{M} \in B \land \forall x \in S 0_{M} +_{M} x = x +_{M} 0_{M}))$
20	7 17 19	mpbir2and	$⊢ (M \in Mnd \land S \subseteq B) \to 0_{M} \in Z (S)$
21		simpll	$⊢ ((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \to M \in Mnd$
22		simprl	$⊢ ((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \to y \in Z (S)$
23	3 22	sseldi	$⊢ ((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \to y \in B$
24		simprr	$⊢ ((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \to z \in Z (S)$
25	3 24	sseldi	$⊢ ((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \to z \in B$
26	1 11	mndcl	$⊢ (M \in Mnd \land y \in B \land z \in B) \to y +_{M} z \in B$
27	21 23 25 26	syl3anc	$⊢ ((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \to y +_{M} z \in B$
28	21	adantr	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to M \in Mnd$
29	23	adantr	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to y \in B$
30	25	adantr	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to z \in B$
31	10	adantlr	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to x \in B$
32	1 11	mndass	$⊢ (M \in Mnd \land (y \in B \land z \in B \land x \in B)) \to (y +_{M} z) +_{M} x = y +_{M} (z +_{M} x)$
33	28 29 30 31 32	syl13anc	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to (y +_{M} z) +_{M} x = y +_{M} (z +_{M} x)$
34	11 2	cntzi	$⊢ (z \in Z (S) \land x \in S) \to z +_{M} x = x +_{M} z$
35	24 34	sylan	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to z +_{M} x = x +_{M} z$
36	35	oveq2d	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to y +_{M} (z +_{M} x) = y +_{M} (x +_{M} z)$
37	1 11	mndass	$⊢ (M \in Mnd \land (y \in B \land x \in B \land z \in B)) \to (y +_{M} x) +_{M} z = y +_{M} (x +_{M} z)$
38	28 29 31 30 37	syl13anc	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to (y +_{M} x) +_{M} z = y +_{M} (x +_{M} z)$
39	11 2	cntzi	$⊢ (y \in Z (S) \land x \in S) \to y +_{M} x = x +_{M} y$
40	22 39	sylan	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to y +_{M} x = x +_{M} y$
41	40	oveq1d	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to (y +_{M} x) +_{M} z = (x +_{M} y) +_{M} z$
42	36 38 41	3eqtr2d	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to y +_{M} (z +_{M} x) = (x +_{M} y) +_{M} z$
43	1 11	mndass	$⊢ (M \in Mnd \land (x \in B \land y \in B \land z \in B)) \to (x +_{M} y) +_{M} z = x +_{M} (y +_{M} z)$
44	28 31 29 30 43	syl13anc	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to (x +_{M} y) +_{M} z = x +_{M} (y +_{M} z)$
45	33 42 44	3eqtrd	$⊢ (((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \land x \in S) \to (y +_{M} z) +_{M} x = x +_{M} (y +_{M} z)$
46	45	ralrimiva	$⊢ ((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \to \forall x \in S (y +_{M} z) +_{M} x = x +_{M} (y +_{M} z)$
47	1 11 2	elcntz	$⊢ S \subseteq B \to (y +_{M} z \in Z (S) \leftrightarrow (y +_{M} z \in B \land \forall x \in S (y +_{M} z) +_{M} x = x +_{M} (y +_{M} z)))$
48	47	ad2antlr	$⊢ ((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \to (y +_{M} z \in Z (S) \leftrightarrow (y +_{M} z \in B \land \forall x \in S (y +_{M} z) +_{M} x = x +_{M} (y +_{M} z)))$
49	27 46 48	mpbir2and	$⊢ ((M \in Mnd \land S \subseteq B) \land (y \in Z (S) \land z \in Z (S))) \to y +_{M} z \in Z (S)$
50	49	ralrimivva	$⊢ (M \in Mnd \land S \subseteq B) \to \forall y \in Z (S) \forall z \in Z (S) y +_{M} z \in Z (S)$
51	1 5 11	issubm	$⊢ M \in Mnd \to (Z (S) \in SubMnd (M) \leftrightarrow (Z (S) \subseteq B \land 0_{M} \in Z (S) \land \forall y \in Z (S) \forall z \in Z (S) y +_{M} z \in Z (S)))$
52	51	adantr	$⊢ (M \in Mnd \land S \subseteq B) \to (Z (S) \in SubMnd (M) \leftrightarrow (Z (S) \subseteq B \land 0_{M} \in Z (S) \land \forall y \in Z (S) \forall z \in Z (S) y +_{M} z \in Z (S)))$
53	4 20 50 52	mpbir3and	$⊢ (M \in Mnd \land S \subseteq B) \to Z (S) \in SubMnd (M)$

Metamath Proof Explorer

Theorem cntzsubm

Proof