Theorem lazval

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

	Ref	Expression
Assertion	lazval	⊢ ( 𝑆 ∈ ℂ → ( Z[]l ‘ 𝑆 ) = { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑠 = 𝑆 → ( 𝑏 · 𝑠 ) = ( 𝑏 · 𝑆 ) )
2	1	oveq2d	⊢ ( 𝑠 = 𝑆 → ( 𝑎 + ( 𝑏 · 𝑠 ) ) = ( 𝑎 + ( 𝑏 · 𝑆 ) ) )
3	2	eqeq2d	⊢ ( 𝑠 = 𝑆 → ( 𝑥 = ( 𝑎 + ( 𝑏 · 𝑠 ) ) ↔ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
4	3	2rexbidv	⊢ ( 𝑠 = 𝑆 → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑠 ) ) ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
5	4	rabbidv	⊢ ( 𝑠 = 𝑆 → { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑠 ) ) } = { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) } )
6		df-laz	⊢ Z[]l = ( 𝑠 ∈ ℂ ↦ { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑠 ) ) } )
7		cnex	⊢ ℂ ∈ V
8	7	rabex	⊢ { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) } ∈ V
9	5 6 8	fvmpt	⊢ ( 𝑆 ∈ ℂ → ( Z[]l ‘ 𝑆 ) = { 𝑥 ∈ ℂ ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) } )