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 ) } )