cntzrcl

Description: Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	cntzrcl.b	$⊢ B = {Base}_{M}$
	cntzrcl.z	$⊢ Z = Cntz (M)$
Assertion	cntzrcl	$⊢ X \in Z (S) \to (M \in V \land S \subseteq B)$

Step	Hyp	Ref	Expression
1		cntzrcl.b	$⊢ B = {Base}_{M}$
2		cntzrcl.z	$⊢ Z = Cntz (M)$
3		noel	$⊢ \neg X \in \emptyset$
4		fvprc	$⊢ \neg M \in V \to Cntz (M) = \emptyset$
5	2 4	eqtrid	$⊢ \neg M \in V \to Z = \emptyset$
6	5	fveq1d	$⊢ \neg M \in V \to Z (S) = \emptyset (S)$
7		0fv	$⊢ \emptyset (S) = \emptyset$
8	6 7	eqtrdi	$⊢ \neg M \in V \to Z (S) = \emptyset$
9	8	eleq2d	$⊢ \neg M \in V \to (X \in Z (S) \leftrightarrow X \in \emptyset)$
10	3 9	mtbiri	$⊢ \neg M \in V \to \neg X \in Z (S)$
11	10	con4i	$⊢ X \in Z (S) \to M \in V$
12		eqid	$⊢ +_{M} = +_{M}$
13	1 12 2	cntzfval	$⊢ M \in V \to Z = (x \in 𝒫 B ⟼ \{y \in B \| \forall z \in x y +_{M} z = z +_{M} y\})$
14	11 13	syl	$⊢ X \in Z (S) \to Z = (x \in 𝒫 B ⟼ \{y \in B \| \forall z \in x y +_{M} z = z +_{M} y\})$
15	14	dmeqd	$⊢ X \in Z (S) \to dom Z = dom (x \in 𝒫 B ⟼ \{y \in B \| \forall z \in x y +_{M} z = z +_{M} y\})$
16		eqid	$⊢ (x \in 𝒫 B ⟼ \{y \in B \| \forall z \in x y +_{M} z = z +_{M} y\}) = (x \in 𝒫 B ⟼ \{y \in B \| \forall z \in x y +_{M} z = z +_{M} y\})$
17	16	dmmptss	$⊢ dom (x \in 𝒫 B ⟼ \{y \in B \| \forall z \in x y +_{M} z = z +_{M} y\}) \subseteq 𝒫 B$
18	15 17	eqsstrdi	$⊢ X \in Z (S) \to dom Z \subseteq 𝒫 B$
19		elfvdm	$⊢ X \in Z (S) \to S \in dom Z$
20	18 19	sseldd	$⊢ X \in Z (S) \to S \in 𝒫 B$
21	20	elpwid	$⊢ X \in Z (S) \to S \subseteq B$
22	11 21	jca	$⊢ X \in Z (S) \to (M \in V \land S \subseteq B)$

Metamath Proof Explorer