Definition df-az 49709

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.)

Assertion

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

Detailed syntax breakdown of Definition df-az

Step	Hyp	Ref	Expression
1		caz 49708	. 2 class Z[]
2		vs	. . 3 setvar 𝑠
3		cc 11235	. . 3 class ℂ
4		cz 12731	. . . . 5 class ℤ
5	2	cv 1569	. . . . . 6 class 𝑠
6	5	csn 4588	. . . . 5 class {𝑠}
7	4, 6	cun 4152	. . . 4 class (ℤ ∪ {𝑠})
8		ccnfld 21720	. . . . 5 class ℂfld
9		crgspn 20904	. . . . 5 class RingSpan
10	8, 9	cfv 6564	. . . 4 class (RingSpan‘ℂfld)
11	7, 10	cfv 6564	. . 3 class ((RingSpan‘ℂfld)‘(ℤ ∪ {𝑠}))
12	2, 3, 11	cmpt 5190	. 2 class (𝑠 ∈ ℂ ↦ ((RingSpan‘ℂfld)‘(ℤ ∪ {𝑠})))
13	1, 12	wceq 1570	1 wff Z[] = (𝑠 ∈ ℂ ↦ ((RingSpan‘ℂfld)‘(ℤ ∪ {𝑠})))

This definition is used by:  azval  49710