Theorem cntrval

Description: Substitute definition of the center. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	cntrval.b	$$⊢B={\mathrm{Base}}_M$$
	cntrval.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
Assertion	cntrval	$$⊢Z\left(B\right)=\mathrm{Cntr}\left(M\right)$$

Proof

Step	Hyp	Ref	Expression
1		cntrval.b	$$⊢B={\mathrm{Base}}_M$$
2		cntrval.z	$$⊢Z=\mathrm{Cntz}\left(M\right)$$
3		fveq2	$$⊢m=M\to \mathrm{Cntz}\left(m\right)=\mathrm{Cntz}\left(M\right)$$
4	3 2	eqtr4di	$$⊢m=M\to \mathrm{Cntz}\left(m\right)=Z$$
5		fveq2	$$⊢m=M\to {\mathrm{Base}}_m={\mathrm{Base}}_M$$
6	5 1	eqtr4di	$$⊢m=M\to {\mathrm{Base}}_m=B$$
7	4 6	fveq12d	$$⊢m=M\to \mathrm{Cntz}\left(m\right)\left({\mathrm{Base}}_m\right)=Z\left(B\right)$$
8		df-cntr	$$⊢\mathrm{Cntr}=\left(m\in \mathrm{V}⟼\mathrm{Cntz}\left(m\right)\left({\mathrm{Base}}_m\right)\right)$$
9		fvex	$$⊢Z\left(B\right)\in \mathrm{V}$$
10	7 8 9	fvmpt	$$⊢M\in \mathrm{V}\to \mathrm{Cntr}\left(M\right)=Z\left(B\right)$$
11	10	eqcomd	$$⊢M\in \mathrm{V}\to Z\left(B\right)=\mathrm{Cntr}\left(M\right)$$
12		0fv	$$⊢\varnothing \left(B\right)=\varnothing$$
13		fvprc	$$⊢\neg M\in \mathrm{V}\to \mathrm{Cntz}\left(M\right)=\varnothing$$
14	2 13	syl5eq	$$⊢\neg M\in \mathrm{V}\to Z=\varnothing$$
15	14	fveq1d	$$⊢\neg M\in \mathrm{V}\to Z\left(B\right)=\varnothing \left(B\right)$$
16		fvprc	$$⊢\neg M\in \mathrm{V}\to \mathrm{Cntr}\left(M\right)=\varnothing$$
17	12 15 16	3eqtr4a	$$⊢\neg M\in \mathrm{V}\to Z\left(B\right)=\mathrm{Cntr}\left(M\right)$$
18	11 17	pm2.61i	$$⊢Z\left(B\right)=\mathrm{Cntr}\left(M\right)$$