Metamath Proof Explorer

Theorem cntzrcl

Description: Reverse closure for elements of the centralizer. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses cntzrcl.b 
|- B = ( Base ` M )
cntzrcl.z 
|- Z = ( Cntz ` M )
Assertion cntzrcl 
|- ( X e. ( Z ` S ) -> ( M e. _V /\ S C_ B ) )

Proof

Step Hyp Ref Expression
1 cntzrcl.b 
 |-  B = ( Base ` M )
2 cntzrcl.z 
 |-  Z = ( Cntz ` M )
3 noel 
 |-  -. X e. (/)
4 fvprc 
 |-  ( -. M e. _V -> ( Cntz ` M ) = (/) )
5 2 4 eqtrid 
 |-  ( -. M e. _V -> Z = (/) )
6 5 fveq1d 
 |-  ( -. M e. _V -> ( Z ` S ) = ( (/) ` S ) )
7 0fv 
 |-  ( (/) ` S ) = (/)
8 6 7 eqtrdi 
 |-  ( -. M e. _V -> ( Z ` S ) = (/) )
9 8 eleq2d 
 |-  ( -. M e. _V -> ( X e. ( Z ` S ) <-> X e. (/) ) )
10 3 9 mtbiri 
 |-  ( -. M e. _V -> -. X e. ( Z ` S ) )
11 10 con4i 
 |-  ( X e. ( Z ` S ) -> M e. _V )
12 eqid 
 |-  ( +g ` M ) = ( +g ` M )
13 1 12 2 cntzfval 
 |-  ( M e. _V -> Z = ( x e. ~P B |-> { y e. B | A. z e. x ( y ( +g ` M ) z ) = ( z ( +g ` M ) y ) } ) )
14 11 13 syl 
 |-  ( X e. ( Z ` S ) -> Z = ( x e. ~P B |-> { y e. B | A. z e. x ( y ( +g ` M ) z ) = ( z ( +g ` M ) y ) } ) )
15 14 dmeqd 
 |-  ( X e. ( Z ` S ) -> dom Z = dom ( x e. ~P B |-> { y e. B | A. z e. x ( y ( +g ` M ) z ) = ( z ( +g ` M ) y ) } ) )
16 eqid 
 |-  ( x e. ~P B |-> { y e. B | A. z e. x ( y ( +g ` M ) z ) = ( z ( +g ` M ) y ) } ) = ( x e. ~P B |-> { y e. B | A. z e. x ( y ( +g ` M ) z ) = ( z ( +g ` M ) y ) } )
17 16 dmmptss 
 |-  dom ( x e. ~P B |-> { y e. B | A. z e. x ( y ( +g ` M ) z ) = ( z ( +g ` M ) y ) } ) C_ ~P B
18 15 17 eqsstrdi 
 |-  ( X e. ( Z ` S ) -> dom Z C_ ~P B )
19 elfvdm 
 |-  ( X e. ( Z ` S ) -> S e. dom Z )
20 18 19 sseldd 
 |-  ( X e. ( Z ` S ) -> S e. ~P B )
21 20 elpwid 
 |-  ( X e. ( Z ` S ) -> S C_ B )
22 11 21 jca 
 |-  ( X e. ( Z ` S ) -> ( M e. _V /\ S C_ B ) )