Definition df-laz 49718

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

Assertion

Ref	Expression
df-laz	⊢ Z[]l = (𝑠 ∈ ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = (𝑎 + (𝑏 · 𝑠))})

Distinct variable group:   𝑎,𝑏,𝑠,𝑥

Detailed syntax breakdown of Definition df-laz

Step	Hyp	Ref	Expression
1		claz 49717	. 2 class Z[]l
2		vs	. . 3 setvar 𝑠
3		cc 11235	. . 3 class ℂ
4		vx	. . . . . . . 8 setvar 𝑥
5	4	cv 1569	. . . . . . 7 class 𝑥
6		va	. . . . . . . . 9 setvar 𝑎
7	6	cv 1569	. . . . . . . 8 class 𝑎
8		vb	. . . . . . . . . 10 setvar 𝑏
9	8	cv 1569	. . . . . . . . 9 class 𝑏
10	2	cv 1569	. . . . . . . . 9 class 𝑠
11		cmul 11242	. . . . . . . . 9 class ·
12	9, 10, 11	co 7449	. . . . . . . 8 class (𝑏 · 𝑠)
13		caddc 11240	. . . . . . . 8 class +
14	7, 12, 13	co 7449	. . . . . . 7 class (𝑎 + (𝑏 · 𝑠))
15	5, 14	wceq 1570	. . . . . 6 wff 𝑥 = (𝑎 + (𝑏 · 𝑠))
16		cz 12731	. . . . . 6 class ℤ
17	15, 8, 16	wrex 3090	. . . . 5 wff ∃𝑏 ∈ ℤ 𝑥 = (𝑎 + (𝑏 · 𝑠))
18	17, 6, 16	wrex 3090	. . . 4 wff ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = (𝑎 + (𝑏 · 𝑠))
19	18, 4, 3	crab 3416	. . 3 class {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = (𝑎 + (𝑏 · 𝑠))}
20	2, 3, 19	cmpt 5190	. 2 class (𝑠 ∈ ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = (𝑎 + (𝑏 · 𝑠))})
21	1, 20	wceq 1570	1 wff Z[]l = (𝑠 ∈ ℂ ↦ {𝑥 ∈ ℂ ∣ ∃𝑎 ∈ ℤ ∃𝑏 ∈ ℤ 𝑥 = (𝑎 + (𝑏 · 𝑠))})

This definition is used by:  lazval  49719