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 
|- B = ( Base ` M )
cntzfval.p 
|- .+ = ( +g ` M )
cntzfval.z 
|- Z = ( Cntz ` M )
Assertion cntzfval 
|- ( M e. V -> Z = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) )

Proof

Step Hyp Ref Expression
1 cntzfval.b 
 |-  B = ( Base ` M )
2 cntzfval.p 
 |-  .+ = ( +g ` M )
3 cntzfval.z 
 |-  Z = ( Cntz ` M )
4 elex 
 |-  ( M e. V -> M e. _V )
5 fveq2 
 |-  ( m = M -> ( Base ` m ) = ( Base ` M ) )
6 5 1 eqtr4di 
 |-  ( m = M -> ( Base ` m ) = B )
7 6 pweqd 
 |-  ( m = M -> ~P ( Base ` m ) = ~P B )
8 fveq2 
 |-  ( m = M -> ( +g ` m ) = ( +g ` M ) )
9 8 2 eqtr4di 
 |-  ( m = M -> ( +g ` m ) = .+ )
10 9 oveqd 
 |-  ( m = M -> ( x ( +g ` m ) y ) = ( x .+ y ) )
11 9 oveqd 
 |-  ( m = M -> ( y ( +g ` m ) x ) = ( y .+ x ) )
12 10 11 eqeq12d 
 |-  ( m = M -> ( ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) <-> ( x .+ y ) = ( y .+ x ) ) )
13 12 ralbidv 
 |-  ( m = M -> ( A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) <-> A. y e. s ( x .+ y ) = ( y .+ x ) ) )
14 6 13 rabeqbidv 
 |-  ( m = M -> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } = { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } )
15 7 14 mpteq12dv 
 |-  ( m = M -> ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } ) = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) )
16 df-cntz 
 |-  Cntz = ( m e. _V |-> ( s e. ~P ( Base ` m ) |-> { x e. ( Base ` m ) | A. y e. s ( x ( +g ` m ) y ) = ( y ( +g ` m ) x ) } ) )
17 1 fvexi 
 |-  B e. _V
18 17 pwex 
 |-  ~P B e. _V
19 18 mptex 
 |-  ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) e. _V
20 15 16 19 fvmpt 
 |-  ( M e. _V -> ( Cntz ` M ) = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) )
21 4 20 syl 
 |-  ( M e. V -> ( Cntz ` M ) = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) )
22 3 21 syl5eq 
 |-  ( M e. V -> Z = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) )