Theorem cntrval

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

	Ref	Expression
Hypotheses	cntrval.b	|- B = ( Base ` M )
	cntrval.z	|- Z = ( Cntz ` M )
Assertion	cntrval	|- ( Z ` B ) = ( Cntr ` M )

Proof

Step	Hyp	Ref	Expression
1		cntrval.b	|- B = ( Base ` M )
2		cntrval.z	|- Z = ( Cntz ` M )
3		fveq2	|- ( m = M -> ( Cntz ` m ) = ( Cntz ` M ) )
4	3 2	eqtr4di	|- ( m = M -> ( Cntz ` m ) = Z )
5		fveq2	|- ( m = M -> ( Base ` m ) = ( Base ` M ) )
6	5 1	eqtr4di	|- ( m = M -> ( Base ` m ) = B )
7	4 6	fveq12d	|- ( m = M -> ( ( Cntz ` m ) ` ( Base ` m ) ) = ( Z ` B ) )
8		df-cntr	|- Cntr = ( m e. _V |-> ( ( Cntz ` m ) ` ( Base ` m ) ) )
9		fvex	|- ( Z ` B ) e. _V
10	7 8 9	fvmpt	|- ( M e. _V -> ( Cntr ` M ) = ( Z ` B ) )
11	10	eqcomd	|- ( M e. _V -> ( Z ` B ) = ( Cntr ` M ) )
12		0fv	|- ( (/) ` B ) = (/)
13		fvprc	|- ( -. M e. _V -> ( Cntz ` M ) = (/) )
14	2 13	syl5eq	|- ( -. M e. _V -> Z = (/) )
15	14	fveq1d	|- ( -. M e. _V -> ( Z ` B ) = ( (/) ` B ) )
16		fvprc	|- ( -. M e. _V -> ( Cntr ` M ) = (/) )
17	12 15 16	3eqtr4a	|- ( -. M e. _V -> ( Z ` B ) = ( Cntr ` M ) )
18	11 17	pm2.61i	|- ( Z ` B ) = ( Cntr ` M )