Metamath Proof Explorer

Theorem lazssaz

Description: A linear adjunction of a complex number to the ring of integers is a subset of the adjunction of the complex number to the ring of integers. (Contributed by AV, 31-Oct-2026)

Ref Expression
Assertion lazssaz ( 𝑆 ∈ ℂ → ( Z[]l ‘ 𝑆 ) ⊆ ( Z[] ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ellazim ⊢ ( ( 𝑆 ∈ ℂ ∧ 𝑥 ∈ ( Z[]l ‘ 𝑆 ) ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) )
2 1 ex ⊢ ( 𝑆 ∈ ℂ → ( 𝑥 ∈ ( Z[]l ‘ 𝑆 ) → ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) ) )
3 zsscn ⊢ ℤ ⊆ ℂ
4 zex ⊢ ℤ ∈ V
5 4 a1i ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ℤ ∈ V )
6 nn0ex ⊢ ℕ0 ∈ V
7 6 a1i ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ℕ0 ∈ V )
8 ifcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ∈ ℤ )
9 8 adantl ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ∈ ℤ )
10 9 adantr ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ 𝑥 ∈ ℕ0 ) → if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ∈ ℤ )
11 eqid ⊢ ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) = ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) )
12 10 11 fmptd ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) : ℕ0 ⟶ ℤ )
13 5 7 12 elmapdd ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ∈ ( ℤ ↑m ℕ0 ) )
14 eqid ⊢ ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) ) = ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) )
15 14 linply ⊢ ( ( ℤ ⊆ ℂ ∧ ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ∈ ( ℤ ↑m ℕ0 ) ) → ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) ) ∈ ( Poly ‘ ℤ ) )
16 3 13 15 sylancr ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) ) ∈ ( Poly ‘ ℤ ) )
17 fveq1 ⊢ ( 𝑝 = ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) ) → ( 𝑝 ‘ 𝑆 ) = ( ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) ) ‘ 𝑆 ) )
18 17 eqeq2d ⊢ ( 𝑝 = ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) ) → ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) = ( 𝑝 ‘ 𝑆 ) ↔ ( 𝑎 + ( 𝑏 · 𝑆 ) ) = ( ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) ) ‘ 𝑆 ) ) )
19 18 adantl ⊢ ( ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) ∧ 𝑝 = ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) ) ) → ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) = ( 𝑝 ‘ 𝑆 ) ↔ ( 𝑎 + ( 𝑏 · 𝑆 ) ) = ( ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) ) ‘ 𝑆 ) ) )
20 simpr ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) )
21 simpl ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑆 ∈ ℂ )
22 14 11 linply2cfv ⊢ ( ( ℤ ⊆ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑆 ∈ ℂ ) → ( ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) ) ‘ 𝑆 ) = ( 𝑎 + ( 𝑏 · 𝑆 ) ) )
23 3 20 21 22 mp3an2i ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) ) ‘ 𝑆 ) = ( 𝑎 + ( 𝑏 · 𝑆 ) ) )
24 23 eqcomd ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 + ( 𝑏 · 𝑆 ) ) = ( ( 𝑐 ∈ ℂ ↦ Σ 𝑖 ∈ ( 0 ... 1 ) ( ( ( 𝑥 ∈ ℕ0 ↦ if ( 𝑥 = 0 , 𝑎 , 𝑏 ) ) ‘ 𝑖 ) · ( 𝑐 ↑ 𝑖 ) ) ) ‘ 𝑆 ) )
25 16 19 24 rspcedvd ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ∃ 𝑝 ∈ ( Poly ‘ ℤ ) ( 𝑎 + ( 𝑏 · 𝑆 ) ) = ( 𝑝 ‘ 𝑆 ) )
26 zsubrg ⊢ ℤ ∈ ( SubRing ‘ ℂfld )
27 26 a1i ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ℤ ∈ ( SubRing ‘ ℂfld ) )
28 eqidd ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) = ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) )
29 27 21 28 rngunsnply ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) ↔ ∃ 𝑝 ∈ ( Poly ‘ ℤ ) ( 𝑎 + ( 𝑏 · 𝑆 ) ) = ( 𝑝 ‘ 𝑆 ) ) )
30 25 29 mpbird ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) )
31 elaz ⊢ ( 𝑆 ∈ ℂ → ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∈ ( Z[] ‘ 𝑆 ) ↔ ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) ) )
32 31 adantr ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∈ ( Z[] ‘ 𝑆 ) ↔ ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∈ ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) ) )
33 30 32 mpbird ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∈ ( Z[] ‘ 𝑆 ) )
34 eleq1 ⊢ ( 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → ( 𝑥 ∈ ( Z[] ‘ 𝑆 ) ↔ ( 𝑎 + ( 𝑏 · 𝑆 ) ) ∈ ( Z[] ‘ 𝑆 ) ) )
35 33 34 syl5ibrcom ⊢ ( ( 𝑆 ∈ ℂ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → 𝑥 ∈ ( Z[] ‘ 𝑆 ) ) )
36 35 rexlimdvva ⊢ ( 𝑆 ∈ ℂ → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ( 𝑎 + ( 𝑏 · 𝑆 ) ) → 𝑥 ∈ ( Z[] ‘ 𝑆 ) ) )
37 2 36 syld ⊢ ( 𝑆 ∈ ℂ → ( 𝑥 ∈ ( Z[]l ‘ 𝑆 ) → 𝑥 ∈ ( Z[] ‘ 𝑆 ) ) )
38 37 ssrdv ⊢ ( 𝑆 ∈ ℂ → ( Z[]l ‘ 𝑆 ) ⊆ ( Z[] ‘ 𝑆 ) )