sscntz

Description: A centralizer expression for two sets elementwise commuting. (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	sscntz	$⊢ (S \subseteq B \land T \subseteq B) \to (S \subseteq Z (T) \leftrightarrow \forall x \in S \forall y \in T 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	cntzval	$⊢ T \subseteq B \to Z (T) = \{x \in B \| \forall y \in T x \underset{˙}{+} y = y \underset{˙}{+} x\}$
5	4	sseq2d	$⊢ T \subseteq B \to (S \subseteq Z (T) \leftrightarrow S \subseteq \{x \in B \| \forall y \in T x \underset{˙}{+} y = y \underset{˙}{+} x\})$
6		ssrab	$⊢ S \subseteq \{x \in B \| \forall y \in T x \underset{˙}{+} y = y \underset{˙}{+} x\} \leftrightarrow (S \subseteq B \land \forall x \in S \forall y \in T x \underset{˙}{+} y = y \underset{˙}{+} x)$
7	5 6	bitrdi	$⊢ T \subseteq B \to (S \subseteq Z (T) \leftrightarrow (S \subseteq B \land \forall x \in S \forall y \in T x \underset{˙}{+} y = y \underset{˙}{+} x))$
8		ibar	$⊢ S \subseteq B \to (\forall x \in S \forall y \in T x \underset{˙}{+} y = y \underset{˙}{+} x \leftrightarrow (S \subseteq B \land \forall x \in S \forall y \in T x \underset{˙}{+} y = y \underset{˙}{+} x))$
9	8	bicomd	$⊢ S \subseteq B \to ((S \subseteq B \land \forall x \in S \forall y \in T x \underset{˙}{+} y = y \underset{˙}{+} x) \leftrightarrow \forall x \in S \forall y \in T x \underset{˙}{+} y = y \underset{˙}{+} x)$
10	7 9	sylan9bbr	$⊢ (S \subseteq B \land T \subseteq B) \to (S \subseteq Z (T) \leftrightarrow \forall x \in S \forall y \in T x \underset{˙}{+} y = y \underset{˙}{+} x)$

Metamath Proof Explorer