elcntz

Description: Elementhood in the centralizer. (Contributed by Mario Carneiro, 22-Sep-2015)

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

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	cntzval	$⊢ S \subseteq B \to Z (S) = \{x \in B \| \forall y \in S x \underset{˙}{+} y = y \underset{˙}{+} x\}$
5	4	eleq2d	$⊢ S \subseteq B \to (A \in Z (S) \leftrightarrow A \in \{x \in B \| \forall y \in S x \underset{˙}{+} y = y \underset{˙}{+} x\})$
6		oveq1	$⊢ x = A \to x \underset{˙}{+} y = A \underset{˙}{+} y$
7		oveq2	$⊢ x = A \to y \underset{˙}{+} x = y \underset{˙}{+} A$
8	6 7	eqeq12d	$⊢ x = A \to (x \underset{˙}{+} y = y \underset{˙}{+} x \leftrightarrow A \underset{˙}{+} y = y \underset{˙}{+} A)$
9	8	ralbidv	$⊢ x = A \to (\forall y \in S x \underset{˙}{+} y = y \underset{˙}{+} x \leftrightarrow \forall y \in S A \underset{˙}{+} y = y \underset{˙}{+} A)$
10	9	elrab	$⊢ A \in \{x \in B \| \forall y \in S x \underset{˙}{+} y = y \underset{˙}{+} x\} \leftrightarrow (A \in B \land \forall y \in S A \underset{˙}{+} y = y \underset{˙}{+} A)$
11	5 10	bitrdi	$⊢ S \subseteq B \to (A \in Z (S) \leftrightarrow (A \in B \land \forall y \in S A \underset{˙}{+} y = y \underset{˙}{+} A))$

Metamath Proof Explorer