Theorem azssid

Description: The union of the integers and the adjoined complex number are a subset of the adjunction. (Contributed by AV, 31-Oct-2026)

	Ref	Expression
Assertion	azssid	⊢ ( 𝑆 ∈ ℂ → ( ℤ ∪ { 𝑆 } ) ⊆ ( Z[] ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		cnring	⊢ ℂfld ∈ Ring
2	1	a1i	⊢ ( 𝑆 ∈ ℂ → ℂfld ∈ Ring )
3		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
4	3	a1i	⊢ ( 𝑆 ∈ ℂ → ℂ = ( Base ‘ ℂfld ) )
5		zsscn	⊢ ℤ ⊆ ℂ
6	5	a1i	⊢ ( 𝑆 ∈ ℂ → ℤ ⊆ ℂ )
7		snssi	⊢ ( 𝑆 ∈ ℂ → { 𝑆 } ⊆ ℂ )
8	6 7	unssd	⊢ ( 𝑆 ∈ ℂ → ( ℤ ∪ { 𝑆 } ) ⊆ ℂ )
9		eqidd	⊢ ( 𝑆 ∈ ℂ → ( RingSpan ‘ ℂfld ) = ( RingSpan ‘ ℂfld ) )
10		azval	⊢ ( 𝑆 ∈ ℂ → ( Z[] ‘ 𝑆 ) = ( ( RingSpan ‘ ℂfld ) ‘ ( ℤ ∪ { 𝑆 } ) ) )
11	2 4 8 9 10	rgspnssid	⊢ ( 𝑆 ∈ ℂ → ( ℤ ∪ { 𝑆 } ) ⊆ ( Z[] ‘ 𝑆 ) )