Theorem azval

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

	Ref	Expression
Assertion	azval	⊢ ( 𝑆 ∈ ℂ → ( Z[] ‘ 𝑆 ) = ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) )

Proof

Step	Hyp	Ref	Expression
1		sneq	⊢ ( 𝑠 = 𝑆 → { 𝑠 } = { 𝑆 } )
2	1	uneq2d	⊢ ( 𝑠 = 𝑆 → ( ℤ ∪ { 𝑠 } ) = ( ℤ ∪ { 𝑆 } ) )
3	2	fveq2d	⊢ ( 𝑠 = 𝑆 → ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑠 } ) ) = ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) )
4		df-az	⊢ Z[] = ( 𝑠 ∈ ℂ ↦ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑠 } ) ) )
5		fvex	⊢ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) ∈ V
6	3 4 5	fvmpt	⊢ ( 𝑆 ∈ ℂ → ( Z[] ‘ 𝑆 ) = ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) )