cntzrec

Description: Reciprocity relationship for centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	cntzrec.b	$⊢ B = {Base}_{M}$
	cntzrec.z	$⊢ Z = Cntz (M)$
Assertion	cntzrec	$⊢ (S \subseteq B \land T \subseteq B) \to (S \subseteq Z (T) \leftrightarrow T \subseteq Z (S))$

Step	Hyp	Ref	Expression
1		cntzrec.b	$⊢ B = {Base}_{M}$
2		cntzrec.z	$⊢ Z = Cntz (M)$
3		ralcom	$⊢ \forall x \in S \forall y \in T x +_{M} y = y +_{M} x \leftrightarrow \forall y \in T \forall x \in S x +_{M} y = y +_{M} x$
4		eqcom	$⊢ x +_{M} y = y +_{M} x \leftrightarrow y +_{M} x = x +_{M} y$
5	4	2ralbii	$⊢ \forall y \in T \forall x \in S x +_{M} y = y +_{M} x \leftrightarrow \forall y \in T \forall x \in S y +_{M} x = x +_{M} y$
6	3 5	bitri	$⊢ \forall x \in S \forall y \in T x +_{M} y = y +_{M} x \leftrightarrow \forall y \in T \forall x \in S y +_{M} x = x +_{M} y$
7	6	a1i	$⊢ (S \subseteq B \land T \subseteq B) \to (\forall x \in S \forall y \in T x +_{M} y = y +_{M} x \leftrightarrow \forall y \in T \forall x \in S y +_{M} x = x +_{M} y)$
8		eqid	$⊢ +_{M} = +_{M}$
9	1 8 2	sscntz	$⊢ (S \subseteq B \land T \subseteq B) \to (S \subseteq Z (T) \leftrightarrow \forall x \in S \forall y \in T x +_{M} y = y +_{M} x)$
10	1 8 2	sscntz	$⊢ (T \subseteq B \land S \subseteq B) \to (T \subseteq Z (S) \leftrightarrow \forall y \in T \forall x \in S y +_{M} x = x +_{M} y)$
11	10	ancoms	$⊢ (S \subseteq B \land T \subseteq B) \to (T \subseteq Z (S) \leftrightarrow \forall y \in T \forall x \in S y +_{M} x = x +_{M} y)$
12	7 9 11	3bitr4d	$⊢ (S \subseteq B \land T \subseteq B) \to (S \subseteq Z (T) \leftrightarrow T \subseteq Z (S))$

Metamath Proof Explorer