Theorem cntzi

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

	Ref	Expression
Hypotheses	cntzi.p	$$⊢\underset{\dot{}}{+}={+}_M$$
	cntzi.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
Assertion	cntzi	$$⊢\left(X\in Z\left(S\right)\wedge Y\in S\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$

Proof

Step	Hyp	Ref	Expression
1		cntzi.p	$$⊢\underset{\dot{}}{+}={+}_M$$
2		cntzi.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
3		eqid	$$⊢{\mathrm{Base}}_M={\mathrm{Base}}_M$$
4	3 2	cntzrcl	$$⊢X\in Z\left(S\right)\to \left(M\in \mathrm{V}\wedge S\subseteq {\mathrm{Base}}_M\right)$$
5	3 1 2	elcntz	$$⊢S\subseteq {\mathrm{Base}}_M\to \left(X\in Z\left(S\right)\leftrightarrow \left(X\in {\mathrm{Base}}_M\wedge \forall y\in SX\underset{\dot{}}{+}y=y\underset{\dot{}}{+}X\right)\right)$$
6	4 5	simpl2im	$$⊢X\in Z\left(S\right)\to \left(X\in Z\left(S\right)\leftrightarrow \left(X\in {\mathrm{Base}}_M\wedge \forall y\in SX\underset{\dot{}}{+}y=y\underset{\dot{}}{+}X\right)\right)$$
7	6	simplbda	$$⊢\left(X\in Z\left(S\right)\wedge X\in Z\left(S\right)\right)\to \forall y\in SX\underset{\dot{}}{+}y=y\underset{\dot{}}{+}X$$
8	7	anidms	$$⊢X\in Z\left(S\right)\to \forall y\in SX\underset{\dot{}}{+}y=y\underset{\dot{}}{+}X$$
9		oveq2	$$⊢y=Y\to X\underset{\dot{}}{+}y=X\underset{\dot{}}{+}Y$$
10		oveq1	$$⊢y=Y\to y\underset{\dot{}}{+}X=Y\underset{\dot{}}{+}X$$
11	9 10	eqeq12d	$$⊢y=Y\to \left(X\underset{\dot{}}{+}y=y\underset{\dot{}}{+}X\leftrightarrow X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X\right)$$
12	11	rspccva	$$⊢\left(\forall y\in SX\underset{\dot{}}{+}y=y\underset{\dot{}}{+}X\wedge Y\in S\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$
13	8 12	sylan	$$⊢\left(X\in Z\left(S\right)\wedge Y\in S\right)\to X\underset{\dot{}}{+}Y=Y\underset{\dot{}}{+}X$$