Theorem azval

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

	Ref	Expression
Assertion	azval	|- ( S e. CC -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) )

Proof

Step	Hyp	Ref	Expression
1		sneq	|- ( s = S -> { s } = { S } )
2	1	uneq2d	|- ( s = S -> ( ZZ u. { s } ) = ( ZZ u. { S } ) )
3	2	fveq2d	|- ( s = S -> ( ( RingSpan ` CCfld ) ` ( ZZ u. { s } ) ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) )
4		df-az	|- Z[] = ( s e. CC |-> ( ( RingSpan ` CCfld ) ` ( ZZ u. { s } ) ) )
5		fvex	|- ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) e. _V
6	3 4 5	fvmpt	|- ( S e. CC -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) )