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	Could not format assertion : No typesetting found for |- Z[] = ( s e. CC |-> ( ( RingSpan ` CCfld ) ` ( ZZ u. { s } ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		caz	Could not format Z[] : No typesetting found for class Z[] with typecode class
1		vs	$$setvars$$
2		cc	$$classℂ$$
3		crgspn	$$class\mathrm{RingSpan}$$
4		ccnfld	$$class{ℂ}_{\mathrm{fld}}$$
5	4 3	cfv	$$class\mathrm{RingSpan}\left({ℂ}_{\mathrm{fld}}\right)$$
6		cz	$$class\mathbb{Z}$$
7	1	cv	$$setvars$$
8	7	csn	$$class\left\{s\right\}$$
9	6 8	cun	$$class\left(\mathbb{Z}\cup \left\{s\right\}\right)$$
10	9 5	cfv	$$class\mathrm{RingSpan}\left({ℂ}_{\mathrm{fld}}\right)\left(\mathbb{Z}\cup \left\{s\right\}\right)$$
11	1 2 10	cmpt	$$class\left(s\in ℂ⟼\mathrm{RingSpan}\left({ℂ}_{\mathrm{fld}}\right)\left(\mathbb{Z}\cup \left\{s\right\}\right)\right)$$
12	0 11	wceq	Could not format Z[] = ( s e. CC |-> ( ( RingSpan ` CCfld ) ` ( ZZ u. { s } ) ) ) : No typesetting found for wff Z[] = ( s e. CC |-> ( ( RingSpan ` CCfld ) ` ( ZZ u. { s } ) ) ) with typecode wff