Theorem cntzval

Description: Definition substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	cntzfval.b	$$⊢B={\mathrm{Base}}_M$$
	cntzfval.p	$$⊢\underset{\dot{}}{+}={+}_M$$
	cntzfval.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
Assertion	cntzval	$$⊢S\subseteq B\to Z\left(S\right)=\left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cntzfval.b	$$⊢B={\mathrm{Base}}_M$$
2		cntzfval.p	$$⊢\underset{\dot{}}{+}={+}_M$$
3		cntzfval.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
4	1 2 3	cntzfval	$$⊢M\in \mathrm{V}\to Z=\left(s\in 𝒫B⟼\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\right)$$
5	4	fveq1d	$$⊢M\in \mathrm{V}\to Z\left(S\right)=\left(s\in 𝒫B⟼\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\right)\left(S\right)$$
6	1	fvexi	$$⊢B\in \mathrm{V}$$
7	6	elpw2	$$⊢S\in 𝒫B\leftrightarrow S\subseteq B$$
8		raleq	$$⊢s=S\to \left(\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\leftrightarrow \forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$
9	8	rabbidv	$$⊢s=S\to \left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}=\left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}$$
10		eqid	$$⊢\left(s\in 𝒫B⟼\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\right)=\left(s\in 𝒫B⟼\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\right)$$
11	6	rabex	$$⊢\left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\in \mathrm{V}$$
12	9 10 11	fvmpt	$$⊢S\in 𝒫B\to \left(s\in 𝒫B⟼\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\right)\left(S\right)=\left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}$$
13	7 12	sylbir	$$⊢S\subseteq B\to \left(s\in 𝒫B⟼\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\right)\left(S\right)=\left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}$$
14	5 13	sylan9eq	$$⊢\left(M\in \mathrm{V}\wedge S\subseteq B\right)\to Z\left(S\right)=\left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}$$
15		0fv	$$⊢\varnothing \left(S\right)=\varnothing$$
16		fvprc	$$⊢\neg M\in \mathrm{V}\to \mathrm{Cntz}\left(M\right)=\varnothing$$
17	3 16	syl5eq	$$⊢\neg M\in \mathrm{V}\to Z=\varnothing$$
18	17	fveq1d	$$⊢\neg M\in \mathrm{V}\to Z\left(S\right)=\varnothing \left(S\right)$$
19		ssrab2	$$⊢\left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\subseteq B$$
20		fvprc	$$⊢\neg M\in \mathrm{V}\to {\mathrm{Base}}_M=\varnothing$$
21	1 20	syl5eq	$$⊢\neg M\in \mathrm{V}\to B=\varnothing$$
22	19 21	sseqtrid	$$⊢\neg M\in \mathrm{V}\to \left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\subseteq \varnothing$$
23		ss0	$$⊢\left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\subseteq \varnothing \to \left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}=\varnothing$$
24	22 23	syl	$$⊢\neg M\in \mathrm{V}\to \left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}=\varnothing$$
25	15 18 24	3eqtr4a	$$⊢\neg M\in \mathrm{V}\to Z\left(S\right)=\left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}$$
26	25	adantr	$$⊢\left(\neg M\in \mathrm{V}\wedge S\subseteq B\right)\to Z\left(S\right)=\left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}$$
27	14 26	pm2.61ian	$$⊢S\subseteq B\to Z\left(S\right)=\left\{x\in B|\forall y\in Sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}$$