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 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 )