cntzsnval

Description: Special substitution for the centralizer of a singleton. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	cntzfval.b	$⊢ B = {Base}_{M}$
	cntzfval.p	$⊢ \underset{˙}{+} = +_{M}$
	cntzfval.z	$⊢ Z = Cntz (M)$
Assertion	cntzsnval	$⊢ Y \in B \to Z (\{Y\}) = \{x \in B \| 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		snssi	$⊢ Y \in B \to \{Y\} \subseteq B$
5	1 2 3	cntzval	$⊢ \{Y\} \subseteq B \to Z (\{Y\}) = \{x \in B \| \forall y \in \{Y\} x \underset{˙}{+} y = y \underset{˙}{+} x\}$
6	4 5	syl	$⊢ Y \in B \to Z (\{Y\}) = \{x \in B \| \forall y \in \{Y\} x \underset{˙}{+} y = y \underset{˙}{+} x\}$
7		oveq2	$⊢ y = Y \to x \underset{˙}{+} y = x \underset{˙}{+} Y$
8		oveq1	$⊢ y = Y \to y \underset{˙}{+} x = Y \underset{˙}{+} x$
9	7 8	eqeq12d	$⊢ y = Y \to (x \underset{˙}{+} y = y \underset{˙}{+} x \leftrightarrow x \underset{˙}{+} Y = Y \underset{˙}{+} x)$
10	9	ralsng	$⊢ Y \in B \to (\forall y \in \{Y\} x \underset{˙}{+} y = y \underset{˙}{+} x \leftrightarrow x \underset{˙}{+} Y = Y \underset{˙}{+} x)$
11	10	rabbidv	$⊢ Y \in B \to \{x \in B \| \forall y \in \{Y\} x \underset{˙}{+} y = y \underset{˙}{+} x\} = \{x \in B \| x \underset{˙}{+} Y = Y \underset{˙}{+} x\}$
12	6 11	eqtrd	$⊢ Y \in B \to Z (\{Y\}) = \{x \in B \| x \underset{˙}{+} Y = Y \underset{˙}{+} x\}$

Metamath Proof Explorer