This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cntzel

Description: Membership in a centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015)

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

Proof

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	elcntz	$⊢ S \subseteq B \to (X \in Z (S) \leftrightarrow (X \in B \land \forall y \in S X \underset{˙}{+} y = y \underset{˙}{+} X))$
5	4	baibd	$⊢ (S \subseteq B \land X \in B) \to (X \in Z (S) \leftrightarrow \forall y \in S X \underset{˙}{+} y = y \underset{˙}{+} X)$