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 eqtrid
 |-  ( M e. V -> Z = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) )