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[] = ( s e. CC |-> ( ( RingSpan ` CCfld ) ` ( ZZ u. { s } ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | caz | |- Z[] |
|
| 1 | vs | |- s |
|
| 2 | cc | |- CC |
|
| 3 | crgspn | |- RingSpan |
|
| 4 | ccnfld | |- CCfld |
|
| 5 | 4 3 | cfv | |- ( RingSpan ` CCfld ) |
| 6 | cz | |- ZZ |
|
| 7 | 1 | cv | |- s |
| 8 | 7 | csn | |- { s } |
| 9 | 6 8 | cun | |- ( ZZ u. { s } ) |
| 10 | 9 5 | cfv | |- ( ( RingSpan ` CCfld ) ` ( ZZ u. { s } ) ) |
| 11 | 1 2 10 | cmpt | |- ( s e. CC |-> ( ( RingSpan ` CCfld ) ` ( ZZ u. { s } ) ) ) |
| 12 | 0 11 | wceq | |- Z[] = ( s e. CC |-> ( ( RingSpan ` CCfld ) ` ( ZZ u. { s } ) ) ) |