Theorem cntziinsn

Description: Express any centralizer as an intersection of singleton centralizers. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	cntzrec.b	|- B = ( Base ` M )
	cntzrec.z	|- Z = ( Cntz ` M )
Assertion	cntziinsn	|- ( S C_ B -> ( Z ` S ) = ( B i^i |^|_ x e. S ( Z ` { x } ) ) )

Proof

Step	Hyp	Ref	Expression
1		cntzrec.b	|- B = ( Base ` M )
2		cntzrec.z	|- Z = ( Cntz ` M )
3		eqid	|- ( +g ` M ) = ( +g ` M )
4	1 3 2	cntzval	|- ( S C_ B -> ( Z ` S ) = { y e. B | A. x e. S ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } )
5		ssel2	|- ( ( S C_ B /\ x e. S ) -> x e. B )
6	1 3 2	cntzsnval	|- ( x e. B -> ( Z ` { x } ) = { y e. B | ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } )
7	5 6	syl	|- ( ( S C_ B /\ x e. S ) -> ( Z ` { x } ) = { y e. B | ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } )
8	7	iineq2dv	|- ( S C_ B -> |^|_ x e. S ( Z ` { x } ) = |^|_ x e. S { y e. B | ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } )
9	8	ineq2d	|- ( S C_ B -> ( B i^i |^|_ x e. S ( Z ` { x } ) ) = ( B i^i |^|_ x e. S { y e. B | ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } ) )
10		riinrab	|- ( B i^i |^|_ x e. S { y e. B | ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } ) = { y e. B | A. x e. S ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) }
11	9 10	eqtrdi	|- ( S C_ B -> ( B i^i |^|_ x e. S ( Z ` { x } ) ) = { y e. B | A. x e. S ( y ( +g ` M ) x ) = ( x ( +g ` M ) y ) } )
12	4 11	eqtr4d	|- ( S C_ B -> ( Z ` S ) = ( B i^i |^|_ x e. S ( Z ` { x } ) ) )