Theorem azval

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

	Ref	Expression
Assertion	azval	Could not format assertion : No typesetting found for |- ( S e. CC -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		sneq	$$⊢s=S\to \left\{s\right\}=\left\{S\right\}$$
2	1	uneq2d	$$⊢s=S\to \mathbb{Z}\cup \left\{s\right\}=\mathbb{Z}\cup \left\{S\right\}$$
3	2	fveq2d	$$⊢s=S\to \mathrm{RingSpan}\left({ℂ}_{\mathrm{fld}}\right)\left(\mathbb{Z}\cup \left\{s\right\}\right)=\mathrm{RingSpan}\left({ℂ}_{\mathrm{fld}}\right)\left(\mathbb{Z}\cup \left\{S\right\}\right)$$
4		df-az	Could not format Z[] = ( s e. CC |-> ( ( RingSpan ` CCfld ) ` ( ZZ u. { s } ) ) ) : No typesetting found for |- Z[] = ( s e. CC |-> ( ( RingSpan ` CCfld ) ` ( ZZ u. { s } ) ) ) with typecode |-
5		fvex	$$⊢\mathrm{RingSpan}\left({ℂ}_{\mathrm{fld}}\right)\left(\mathbb{Z}\cup \left\{S\right\}\right)\in \mathrm{V}$$
6	3 4 5	fvmpt	Could not format ( S e. CC -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) : No typesetting found for |- ( S e. CC -> ( Z[] ` S ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) with typecode |-