Metamath Proof Explorer

Definition df-laz

Description: Define the mapping yielding the adjunctions of a complex number to the ring of integers. Analogous to df-gz . (Contributed by AV, 24-Oct-2026)

Ref Expression
Assertion df-laz 
|- Z[]l = ( s e. CC |-> { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. s ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 claz 
 |-  Z[]l
1 vs 
 |-  s
2 cc 
 |-  CC
3 vx 
 |-  x
4 va 
 |-  a
5 cz 
 |-  ZZ
6 vb 
 |-  b
7 3 cv 
 |-  x
8 4 cv 
 |-  a
9 caddc 
 |-  +
10 6 cv 
 |-  b
11 cmul 
 |-  x.
12 1 cv 
 |-  s
13 10 12 11 co 
 |-  ( b x. s )
14 8 13 9 co 
 |-  ( a + ( b x. s ) )
15 7 14 wceq 
 |-  x = ( a + ( b x. s ) )
16 15 6 5 wrex 
 |-  E. b e. ZZ x = ( a + ( b x. s ) )
17 16 4 5 wrex 
 |-  E. a e. ZZ E. b e. ZZ x = ( a + ( b x. s ) )
18 17 3 2 crab 
 |-  { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. s ) ) }
19 1 2 18 cmpt 
 |-  ( s e. CC |-> { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. s ) ) } )
20 0 19 wceq 
 |-  Z[]l = ( s e. CC |-> { x e. CC | E. a e. ZZ E. b e. ZZ x = ( a + ( b x. s ) ) } )