cntzcmn

Description: The centralizer of any subset in a commutative monoid is the whole monoid. (Contributed by Mario Carneiro, 3-Oct-2015)

	Ref	Expression
Hypotheses	cntzcmn.b	$⊢ B = {Base}_{G}$
	cntzcmn.z	$⊢ Z = Cntz (G)$
Assertion	cntzcmn	$⊢ (G \in CMnd \land S \subseteq B) \to Z (S) = B$

Step	Hyp	Ref	Expression
1		cntzcmn.b	$⊢ B = {Base}_{G}$
2		cntzcmn.z	$⊢ Z = Cntz (G)$
3	1 2	cntzssv	$⊢ Z (S) \subseteq B$
4	3	a1i	$⊢ (G \in CMnd \land S \subseteq B) \to Z (S) \subseteq B$
5		simpl1	$⊢ ((G \in CMnd \land S \subseteq B \land x \in B) \land y \in S) \to G \in CMnd$
6		simpl3	$⊢ ((G \in CMnd \land S \subseteq B \land x \in B) \land y \in S) \to x \in B$
7		simp2	$⊢ (G \in CMnd \land S \subseteq B \land x \in B) \to S \subseteq B$
8	7	sselda	$⊢ ((G \in CMnd \land S \subseteq B \land x \in B) \land y \in S) \to y \in B$
9		eqid	$⊢ +_{G} = +_{G}$
10	1 9	cmncom	$⊢ (G \in CMnd \land x \in B \land y \in B) \to x +_{G} y = y +_{G} x$
11	5 6 8 10	syl3anc	$⊢ ((G \in CMnd \land S \subseteq B \land x \in B) \land y \in S) \to x +_{G} y = y +_{G} x$
12	11	ralrimiva	$⊢ (G \in CMnd \land S \subseteq B \land x \in B) \to \forall y \in S x +_{G} y = y +_{G} x$
13	1 9 2	cntzel	$⊢ (S \subseteq B \land x \in B) \to (x \in Z (S) \leftrightarrow \forall y \in S x +_{G} y = y +_{G} x)$
14	13	3adant1	$⊢ (G \in CMnd \land S \subseteq B \land x \in B) \to (x \in Z (S) \leftrightarrow \forall y \in S x +_{G} y = y +_{G} x)$
15	12 14	mpbird	$⊢ (G \in CMnd \land S \subseteq B \land x \in B) \to x \in Z (S)$
16	15	3expia	$⊢ (G \in CMnd \land S \subseteq B) \to (x \in B \to x \in Z (S))$
17	16	ssrdv	$⊢ (G \in CMnd \land S \subseteq B) \to B \subseteq Z (S)$
18	4 17	eqssd	$⊢ (G \in CMnd \land S \subseteq B) \to Z (S) = B$

Metamath Proof Explorer