Definition df-az

Description: Define the mapping yielding the adjunctions of a complex number to the ring of integers. See also Wikipedia https://en.wikipedia.org/wiki/Subring#Adjoining . (Proposed by TA, 29-Oct-2026.) (Contributed by AV, 30-Oct-2026)

	Ref	Expression
Assertion	df-az	⊢ Z[] = ( 𝑠 ∈ ℂ ↦ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑠 } ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		caz	⊢ Z[]
1		vs	⊢ 𝑠
2		cc	⊢ ℂ
3		crgspn	⊢ RingSpan
4		ccnfld	⊢ ℂfld
5	4 3	cfv	⊢ ( RingSpan ‘ ℂfld )
6		cz	⊢ ℤ
7	1	cv	⊢ 𝑠
8	7	csn	⊢ { 𝑠 }
9	6 8	cun	⊢ ( ℤ ∪ { 𝑠 } )
10	9 5	cfv	⊢ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑠 } ) )
11	1 2 10	cmpt	⊢ ( 𝑠 ∈ ℂ ↦ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑠 } ) ) )
12	0 11	wceq	⊢ Z[] = ( 𝑠 ∈ ℂ ↦ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑠 } ) ) )