elcntzsn

Description: Value of the centralizer of a singleton. (Contributed by Mario Carneiro, 25-Apr-2016)

	Ref	Expression
Hypotheses	cntzfval.b	$⊢ B = {Base}_{M}$
	cntzfval.p	$⊢ \underset{˙}{+} = +_{M}$
	cntzfval.z	$⊢ Z = Cntz (M)$
Assertion	elcntzsn	$⊢ Y \in B \to (X \in Z (\{Y\}) \leftrightarrow (X \in B \land X \underset{˙}{+} Y = Y \underset{˙}{+} X))$

Step	Hyp	Ref	Expression
1		cntzfval.b	$⊢ B = {Base}_{M}$
2		cntzfval.p	$⊢ \underset{˙}{+} = +_{M}$
3		cntzfval.z	$⊢ Z = Cntz (M)$
4	1 2 3	cntzsnval	$⊢ Y \in B \to Z (\{Y\}) = \{x \in B \| x \underset{˙}{+} Y = Y \underset{˙}{+} x\}$
5	4	eleq2d	$⊢ Y \in B \to (X \in Z (\{Y\}) \leftrightarrow X \in \{x \in B \| x \underset{˙}{+} Y = Y \underset{˙}{+} x\})$
6		oveq1	$⊢ x = X \to x \underset{˙}{+} Y = X \underset{˙}{+} Y$
7		oveq2	$⊢ x = X \to Y \underset{˙}{+} x = Y \underset{˙}{+} X$
8	6 7	eqeq12d	$⊢ x = X \to (x \underset{˙}{+} Y = Y \underset{˙}{+} x \leftrightarrow X \underset{˙}{+} Y = Y \underset{˙}{+} X)$
9	8	elrab	$⊢ X \in \{x \in B \| x \underset{˙}{+} Y = Y \underset{˙}{+} x\} \leftrightarrow (X \in B \land X \underset{˙}{+} Y = Y \underset{˙}{+} X)$
10	5 9	bitrdi	$⊢ Y \in B \to (X \in Z (\{Y\}) \leftrightarrow (X \in B \land X \underset{˙}{+} Y = Y \underset{˙}{+} X))$

Metamath Proof Explorer