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

Metamath Proof Explorer

Theorem cntzfval

Description: First level substitution for a centralizer. (Contributed by Stefan O'Rear, 5-Sep-2015)

Ref Expression
Hypotheses cntzfval.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
cntzfval.p ⊢ + = ( +g ‘ 𝑀 )
cntzfval.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion cntzfval ( 𝑀 ∈ 𝑉 → 𝑍 = ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) )

Proof

Step Hyp Ref Expression
1 cntzfval.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 cntzfval.p ⊢ + = ( +g ‘ 𝑀 )
3 cntzfval.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
4 elex ⊢ ( 𝑀 ∈ 𝑉 → 𝑀 ∈ V )
5 fveq2 ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = ( Base ‘ 𝑀 ) )
6 5 1 eqtr4di ⊢ ( 𝑚 = 𝑀 → ( Base ‘ 𝑚 ) = 𝐵 )
7 6 pweqd ⊢ ( 𝑚 = 𝑀 → 𝒫 ( Base ‘ 𝑚 ) = 𝒫 𝐵 )
8 fveq2 ⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) = ( +g ‘ 𝑀 ) )
9 8 2 eqtr4di ⊢ ( 𝑚 = 𝑀 → ( +g ‘ 𝑚 ) = + )
10 9 oveqd ⊢ ( 𝑚 = 𝑀 → ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑥 + 𝑦 ) )
11 9 oveqd ⊢ ( 𝑚 = 𝑀 → ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) = ( 𝑦 + 𝑥 ) )
12 10 11 eqeq12d ⊢ ( 𝑚 = 𝑀 → ( ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) ↔ ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
13 12 ralbidv ⊢ ( 𝑚 = 𝑀 → ( ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) ) )
14 6 13 rabeqbidv ⊢ ( 𝑚 = 𝑀 → { 𝑥 ∈ ( Base ‘ 𝑚 ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) } = { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } )
15 7 14 mpteq12dv ⊢ ( 𝑚 = 𝑀 → ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑚 ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) } ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) )
16 df-cntz ⊢ Cntz = ( 𝑚 ∈ V ↦ ( 𝑠 ∈ 𝒫 ( Base ‘ 𝑚 ) ↦ { 𝑥 ∈ ( Base ‘ 𝑚 ) ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 ( +g ‘ 𝑚 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑚 ) 𝑥 ) } ) )
17 1 fvexi ⊢ 𝐵 ∈ V
18 17 pwex ⊢ 𝒫 𝐵 ∈ V
19 18 mptex ⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) ∈ V
20 15 16 19 fvmpt ⊢ ( 𝑀 ∈ V → ( Cntz ‘ 𝑀 ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) )
21 4 20 syl ⊢ ( 𝑀 ∈ 𝑉 → ( Cntz ‘ 𝑀 ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) )
22 3 21 eqtrid ⊢ ( 𝑀 ∈ 𝑉 → 𝑍 = ( 𝑠 ∈ 𝒫 𝐵 ↦ { 𝑥 ∈ 𝐵 ∣ ∀ 𝑦 ∈ 𝑠 ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) } ) )