This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid 
 |-  ( -. 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 )