Theorem lazval

Description: An adjunction of a complex number to the ring of integers. (Contributed by AV, 24-Oct-2026)

	Ref	Expression
Assertion	lazval	|- ( S e. CC -> ( Z[]l ` S ) = { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) } )

Proof

Step	Hyp	Ref	Expression
1		oveq2	|- ( s = S -> ( b x. s ) = ( b x. S ) )
2	1	oveq2d	|- ( s = S -> ( a + ( b x. s ) ) = ( a + ( b x. S ) ) )
3	2	eqeq2d	|- ( s = S -> ( x = ( a + ( b x. s ) ) <-> x = ( a + ( b x. S ) ) ) )
4	3	2rexbidv	|- ( s = S -> ( E. a e. ZZ E. b e. ZZ x = ( a + ( b x. s ) ) <-> E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) ) )
5	4	rabbidv	|- ( s = S -> { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. s ) ) } = { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) } )
6		df-laz	|- Z[]l = ( s e. CC |-> { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. s ) ) } )
7		cnex	|- CC e. _V
8	7	rabex	|- { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) } e. _V
9	5 6 8	fvmpt	|- ( S e. CC -> ( Z[]l ` S ) = { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) } )