Theorem cntzfval

Description: First level 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	cntzfval	$$⊢M\in V\to Z=\left(s\in 𝒫B⟼\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\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		elex	$$⊢M\in V\to M\in \mathrm{V}$$
5		fveq2	$$⊢m=M\to {\mathrm{Base}}_m={\mathrm{Base}}_M$$
6	5 1	eqtr4di	$$⊢m=M\to {\mathrm{Base}}_m=B$$
7	6	pweqd	$$⊢m=M\to 𝒫{\mathrm{Base}}_m=𝒫B$$
8		fveq2	$$⊢m=M\to {+}_m={+}_M$$
9	8 2	eqtr4di	$$⊢m=M\to {+}_m=\underset{\dot{}}{+}$$
10	9	oveqd	$$⊢m=M\to x{+}_{m}y=x\underset{\dot{}}{+}y$$
11	9	oveqd	$$⊢m=M\to y{+}_{m}x=y\underset{\dot{}}{+}x$$
12	10 11	eqeq12d	$$⊢m=M\to \left(x{+}_{m}y=y{+}_{m}x\leftrightarrow x\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$
13	12	ralbidv	$$⊢m=M\to \left(\forall y\in sx{+}_{m}y=y{+}_{m}x\leftrightarrow \forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right)$$
14	6 13	rabeqbidv	$$⊢m=M\to \left\{x\in {\mathrm{Base}}_m|\forall y\in sx{+}_{m}y=y{+}_{m}x\right\}=\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}$$
15	7 14	mpteq12dv	$$⊢m=M\to \left(s\in 𝒫{\mathrm{Base}}_m⟼\left\{x\in {\mathrm{Base}}_m|\forall y\in sx{+}_{m}y=y{+}_{m}x\right\}\right)=\left(s\in 𝒫B⟼\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\right)$$
16		df-cntz	$$⊢\mathrm{Cntz}=\left(m\in \mathrm{V}⟼\left(s\in 𝒫{\mathrm{Base}}_m⟼\left\{x\in {\mathrm{Base}}_m|\forall y\in sx{+}_{m}y=y{+}_{m}x\right\}\right)\right)$$
17	1	fvexi	$$⊢B\in \mathrm{V}$$
18	17	pwex	$$⊢𝒫B\in \mathrm{V}$$
19	18	mptex	$$⊢\left(s\in 𝒫B⟼\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\right)\in \mathrm{V}$$
20	15 16 19	fvmpt	$$⊢M\in \mathrm{V}\to \mathrm{Cntz}\left(M\right)=\left(s\in 𝒫B⟼\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\right)$$
21	4 20	syl	$$⊢M\in V\to \mathrm{Cntz}\left(M\right)=\left(s\in 𝒫B⟼\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\right)$$
22	3 21	syl5eq	$$⊢M\in V\to Z=\left(s\in 𝒫B⟼\left\{x\in B|\forall y\in sx\underset{\dot{}}{+}y=y\underset{\dot{}}{+}x\right\}\right)$$