Theorem cntzsnval

Description: Special substitution for the centralizer of a singleton. (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	cntzsnval	|- ( Y e. B -> ( Z ` { Y } ) = { x e. B | ( 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		snssi	|- ( Y e. B -> { Y } C_ B )
5	1 2 3	cntzval	|- ( { Y } C_ B -> ( Z ` { Y } ) = { x e. B | A. y e. { Y } ( x .+ y ) = ( y .+ x ) } )
6	4 5	syl	|- ( Y e. B -> ( Z ` { Y } ) = { x e. B | A. y e. { Y } ( x .+ y ) = ( y .+ x ) } )
7		oveq2	|- ( y = Y -> ( x .+ y ) = ( x .+ Y ) )
8		oveq1	|- ( y = Y -> ( y .+ x ) = ( Y .+ x ) )
9	7 8	eqeq12d	|- ( y = Y -> ( ( x .+ y ) = ( y .+ x ) <-> ( x .+ Y ) = ( Y .+ x ) ) )
10	9	ralsng	|- ( Y e. B -> ( A. y e. { Y } ( x .+ y ) = ( y .+ x ) <-> ( x .+ Y ) = ( Y .+ x ) ) )
11	10	rabbidv	|- ( Y e. B -> { x e. B | A. y e. { Y } ( x .+ y ) = ( y .+ x ) } = { x e. B | ( x .+ Y ) = ( Y .+ x ) } )
12	6 11	eqtrd	|- ( Y e. B -> ( Z ` { Y } ) = { x e. B | ( x .+ Y ) = ( Y .+ x ) } )