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	Could not format assertion : No typesetting found for |- ( S e. CC -> ( Z[]l ` S ) C_ ( Z[] ` S ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ellazim	Could not format ( ( S e. CC /\ x e. ( Z[]l ` S ) ) -> E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) ) : No typesetting found for |- ( ( S e. CC /\ x e. ( Z[]l ` S ) ) -> E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) ) with typecode |-
2	1	ex	Could not format ( S e. CC -> ( x e. ( Z[]l ` S ) -> E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) ) ) : No typesetting found for |- ( S e. CC -> ( x e. ( Z[]l ` S ) -> E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) ) ) with typecode |-
3		zsscn	$$⊢\mathbb{Z}\subseteq ℂ$$
4		zex	$$⊢\mathbb{Z}\in \mathrm{V}$$
5	4	a1i	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to \mathbb{Z}\in \mathrm{V}$$
6		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
7	6	a1i	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to {\mathbb{N}}_0\in \mathrm{V}$$
8		ifcl	$$⊢\left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\to if\left(x=0,a,b\right)\in \mathbb{Z}$$
9	8	adantl	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to if\left(x=0,a,b\right)\in \mathbb{Z}$$
10	9	adantr	$$⊢\left(\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\wedge x\in {\mathbb{N}}_0\right)\to if\left(x=0,a,b\right)\in \mathbb{Z}$$
11		eqid	$$⊢\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)=\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)$$
12	10 11	fmptd	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to \left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right):{\mathbb{N}}_0⟶\mathbb{Z}$$
13	5 7 12	elmapdd	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to \left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\in \left({\mathbb{Z}}^{{\mathbb{N}}_0}\right)$$
14		eqid	$$⊢\left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)=\left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)$$
15	14	linply	$$⊢\left(\mathbb{Z}\subseteq ℂ\wedge \left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\in \left({\mathbb{Z}}^{{\mathbb{N}}_0}\right)\right)\to \left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)\in \mathrm{Poly}\left(\mathbb{Z}\right)$$
16	3 13 15	sylancr	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to \left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)\in \mathrm{Poly}\left(\mathbb{Z}\right)$$
17		fveq1	$$⊢p=\left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)\to p\left(S\right)=\left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)\left(S\right)$$
18	17	eqeq2d	$$⊢p=\left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)\to \left(a+bS=p\left(S\right)\leftrightarrow a+bS=\left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)\left(S\right)\right)$$
19	18	adantl	$$⊢\left(\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\wedge p=\left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)\right)\to \left(a+bS=p\left(S\right)\leftrightarrow a+bS=\left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)\left(S\right)\right)$$
20		simpr	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)$$
21		simpl	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to S\in ℂ$$
22	14 11	linply2cfv	$$⊢\left(\mathbb{Z}\subseteq ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\wedge S\in ℂ\right)\to \left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)\left(S\right)=a+bS$$
23	3 20 21 22	mp3an2i	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to \left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)\left(S\right)=a+bS$$
24	23	eqcomd	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to a+bS=\left(c\in ℂ⟼\sum _{i=0}^1\left(x\in {\mathbb{N}}_0⟼if\left(x=0,a,b\right)\right)\left(i\right)c^i\right)\left(S\right)$$
25	16 19 24	rspcedvd	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to \exists p\in \mathrm{Poly}\left(\mathbb{Z}\right)a+bS=p\left(S\right)$$
26		zsubrg	$$⊢\mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
27	26	a1i	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to \mathbb{Z}\in \mathrm{SubRing}\left({ℂ}_{\mathrm{fld}}\right)$$
28		eqidd	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to \mathrm{RingSpan}\left({ℂ}_{\mathrm{fld}}\right)\left(\mathbb{Z}\cup \left\{S\right\}\right)=\mathrm{RingSpan}\left({ℂ}_{\mathrm{fld}}\right)\left(\mathbb{Z}\cup \left\{S\right\}\right)$$
29	27 21 28	rngunsnply	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to \left(a+bS\in \mathrm{RingSpan}\left({ℂ}_{\mathrm{fld}}\right)\left(\mathbb{Z}\cup \left\{S\right\}\right)\leftrightarrow \exists p\in \mathrm{Poly}\left(\mathbb{Z}\right)a+bS=p\left(S\right)\right)$$
30	25 29	mpbird	$$⊢\left(S\in ℂ\wedge \left(a\in \mathbb{Z}\wedge b\in \mathbb{Z}\right)\right)\to a+bS\in \mathrm{RingSpan}\left({ℂ}_{\mathrm{fld}}\right)\left(\mathbb{Z}\cup \left\{S\right\}\right)$$
31		elaz	Could not format ( S e. CC -> ( ( a + ( b x. S ) ) e. ( Z[] ` S ) <-> ( a + ( b x. S ) ) e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) ) : No typesetting found for |- ( S e. CC -> ( ( a + ( b x. S ) ) e. ( Z[] ` S ) <-> ( a + ( b x. S ) ) e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) ) with typecode |-
32	31	adantr	Could not format ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a + ( b x. S ) ) e. ( Z[] ` S ) <-> ( a + ( b x. S ) ) e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) ) : No typesetting found for |- ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a + ( b x. S ) ) e. ( Z[] ` S ) <-> ( a + ( b x. S ) ) e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) ) with typecode |-
33	30 32	mpbird	Could not format ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a + ( b x. S ) ) e. ( Z[] ` S ) ) : No typesetting found for |- ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a + ( b x. S ) ) e. ( Z[] ` S ) ) with typecode |-
34		eleq1	Could not format ( x = ( a + ( b x. S ) ) -> ( x e. ( Z[] ` S ) <-> ( a + ( b x. S ) ) e. ( Z[] ` S ) ) ) : No typesetting found for |- ( x = ( a + ( b x. S ) ) -> ( x e. ( Z[] ` S ) <-> ( a + ( b x. S ) ) e. ( Z[] ` S ) ) ) with typecode |-
35	33 34	syl5ibrcom	Could not format ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( x = ( a + ( b x. S ) ) -> x e. ( Z[] ` S ) ) ) : No typesetting found for |- ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( x = ( a + ( b x. S ) ) -> x e. ( Z[] ` S ) ) ) with typecode |-
36	35	rexlimdvva	Could not format ( S e. CC -> ( E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) -> x e. ( Z[] ` S ) ) ) : No typesetting found for |- ( S e. CC -> ( E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) -> x e. ( Z[] ` S ) ) ) with typecode |-
37	2 36	syld	Could not format ( S e. CC -> ( x e. ( Z[]l ` S ) -> x e. ( Z[] ` S ) ) ) : No typesetting found for |- ( S e. CC -> ( x e. ( Z[]l ` S ) -> x e. ( Z[] ` S ) ) ) with typecode |-
38	37	ssrdv	Could not format ( S e. CC -> ( Z[]l ` S ) C_ ( Z[] ` S ) ) : No typesetting found for |- ( S e. CC -> ( Z[]l ` S ) C_ ( Z[] ` S ) ) with typecode |-