Metamath Proof Explorer

Theorem cntzval

Description: Definition 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 cntzval 
|- ( S C_ B -> ( Z ` S ) = { 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 1 2 3 cntzfval 
 |-  ( M e. _V -> Z = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) )
5 4 fveq1d 
 |-  ( M e. _V -> ( Z ` S ) = ( ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) ` S ) )
6 1 fvexi 
 |-  B e. _V
7 6 elpw2 
 |-  ( S e. ~P B <-> S C_ B )
8 raleq 
 |-  ( s = S -> ( A. y e. s ( x .+ y ) = ( y .+ x ) <-> A. y e. S ( x .+ y ) = ( y .+ x ) ) )
9 8 rabbidv 
 |-  ( s = S -> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } )
10 eqid 
 |-  ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) = ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } )
11 6 rabex 
 |-  { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } e. _V
12 9 10 11 fvmpt 
 |-  ( S e. ~P B -> ( ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } )
13 7 12 sylbir 
 |-  ( S C_ B -> ( ( s e. ~P B |-> { x e. B | A. y e. s ( x .+ y ) = ( y .+ x ) } ) ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } )
14 5 13 sylan9eq 
 |-  ( ( M e. _V /\ S C_ B ) -> ( Z ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } )
15 0fv 
 |-  ( (/) ` S ) = (/)
16 fvprc 
 |-  ( -. M e. _V -> ( Cntz ` M ) = (/) )
17 3 16 eqtrid 
 |-  ( -. M e. _V -> Z = (/) )
18 17 fveq1d 
 |-  ( -. M e. _V -> ( Z ` S ) = ( (/) ` S ) )
19 ssrab2 
 |-  { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } C_ B
20 fvprc 
 |-  ( -. M e. _V -> ( Base ` M ) = (/) )
21 1 20 eqtrid 
 |-  ( -. M e. _V -> B = (/) )
22 19 21 sseqtrid 
 |-  ( -. M e. _V -> { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } C_ (/) )
23 ss0 
 |-  ( { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } C_ (/) -> { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } = (/) )
24 22 23 syl 
 |-  ( -. M e. _V -> { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } = (/) )
25 15 18 24 3eqtr4a 
 |-  ( -. M e. _V -> ( Z ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } )
26 25 adantr 
 |-  ( ( -. M e. _V /\ S C_ B ) -> ( Z ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } )
27 14 26 pm2.61ian 
 |-  ( S C_ B -> ( Z ` S ) = { x e. B | A. y e. S ( x .+ y ) = ( y .+ x ) } )