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 ⊢ 𝐵 = ( Base ‘ 𝑀 )
cntrval.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion cntrval ( 𝑍 ‘ 𝐵 ) = ( Cntr ‘ 𝑀 )

Proof

Step Hyp Ref Expression
1 cntrval.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 cntrval.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3 fveq2 ⊢ ( 𝑚 = 𝑀 → ( Cntz ‘ 𝑚 ) = ( Cntz ‘ 𝑀 ) )
4 3 2 eqtr4di ⊢ ( 𝑚 = 𝑀 → ( Cntz ‘ 𝑚 ) = 𝑍 )
5 fveq2 ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
6 5 1 eqtr4di ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = 𝐵 )
7 4 6 fveq12d ⊢ ( 𝑚 = 𝑀 → ( ( Cntz ‘ 𝑚 ) ‘ ( Base ‘ 𝑚 ) ) = ( 𝑍 ‘ 𝐵 ) )
8 df-cntr ⊢ Cntr = ( 𝑚 ∈ V ↦ ( ( Cntz ‘ 𝑚 ) ‘ ( Base ‘ 𝑚 ) ) )
9 fvex ⊢ ( 𝑍 ‘ 𝐵 ) ∈ V
10 7 8 9 fvmpt ⊢ ( 𝑀 ∈ V → ( Cntr ‘ 𝑀 ) = ( 𝑍 ‘ 𝐵 ) )
11 10 eqcomd ⊢ ( 𝑀 ∈ V → ( 𝑍 ‘ 𝐵 ) = ( Cntr ‘ 𝑀 ) )
12 0fv ⊢ ( ∅ ‘ 𝐵 ) = ∅
13 fvprc ⊢ ( ¬ 𝑀 ∈ V → ( Cntz ‘ 𝑀 ) = ∅ )
14 2 13 eqtrid ⊢ ( ¬ 𝑀 ∈ V → 𝑍 = ∅ )
15 14 fveq1d ⊢ ( ¬ 𝑀 ∈ V → ( 𝑍 ‘ 𝐵 ) = ( ∅ ‘ 𝐵 ) )
16 fvprc ⊢ ( ¬ 𝑀 ∈ V → ( Cntr ‘ 𝑀 ) = ∅ )
17 12 15 16 3eqtr4a ⊢ ( ¬ 𝑀 ∈ V → ( 𝑍 ‘ 𝐵 ) = ( Cntr ‘ 𝑀 ) )
18 11 17 pm2.61i ⊢ ( 𝑍 ‘ 𝐵 ) = ( Cntr ‘ 𝑀 )