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 = ( 𝑠 ∈ ℂ ↦ { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑠 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		claz	⊢ Z[]l
1		vs	⊢ 𝑠
2		cc	⊢ ℂ
3		vx	⊢ 𝑥
4		va	⊢ 𝑎
5		cz	⊢ ℤ
6		vb	⊢ 𝑏
7	3	cv	⊢ 𝑥
8	4	cv	⊢ 𝑎
9		caddc	⊢ +
10	6	cv	⊢ 𝑏
11		cmul	⊢ ·
12	1	cv	⊢ 𝑠
13	10 12 11	co	⊢ ( 𝑏 · 𝑠 )
14	8 13 9	co	⊢ ( 𝑎 + ( 𝑏 · 𝑠 ) )
15	7 14	wceq	⊢ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑠 ) )
16	15 6 5	wrex	⊢ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑠 ) )
17	16 4 5	wrex	⊢ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑠 ) )
18	17 3 2	crab	⊢ { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑠 ) ) }
19	1 2 18	cmpt	⊢ ( 𝑠 ∈ ℂ ↦ { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑠 ) ) } )
20	0 19	wceq	⊢ Z[]l = ( 𝑠 ∈ ℂ ↦ { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑠 ) ) } )