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 
|- ( S e. CC -> ( Z[]l ` S ) C_ ( Z[] ` S ) )

Proof

Step Hyp Ref Expression
1 ellazim 
 |-  ( ( S e. CC /\ x e. ( Z[]l ` S ) ) -> E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) )
2 1 ex 
 |-  ( S e. CC -> ( x e. ( Z[]l ` S ) -> E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) ) )
3 zsscn 
 |-  ZZ C_ CC
4 zex 
 |-  ZZ e. _V
5 4 a1i 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ZZ e. _V )
6 nn0ex 
 |-  NN0 e. _V
7 6 a1i 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> NN0 e. _V )
8 ifcl 
 |-  ( ( a e. ZZ /\ b e. ZZ ) -> if ( x = 0 , a , b ) e. ZZ )
9 8 adantl 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> if ( x = 0 , a , b ) e. ZZ )
10 9 adantr 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ x e. NN0 ) -> if ( x = 0 , a , b ) e. ZZ )
11 eqid 
 |-  ( x e. NN0 |-> if ( x = 0 , a , b ) ) = ( x e. NN0 |-> if ( x = 0 , a , b ) )
12 10 11 fmptd 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( x e. NN0 |-> if ( x = 0 , a , b ) ) : NN0 --> ZZ )
13 5 7 12 elmapdd 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( x e. NN0 |-> if ( x = 0 , a , b ) ) e. ( ZZ ^m NN0 ) )
14 eqid 
 |-  ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) ) = ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) )
15 14 linply 
 |-  ( ( ZZ C_ CC /\ ( x e. NN0 |-> if ( x = 0 , a , b ) ) e. ( ZZ ^m NN0 ) ) -> ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) ) e. ( Poly ` ZZ ) )
16 3 13 15 sylancr 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) ) e. ( Poly ` ZZ ) )
17 fveq1 
 |-  ( p = ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) ) -> ( p ` S ) = ( ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) ) ` S ) )
18 17 eqeq2d 
 |-  ( p = ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) ) -> ( ( a + ( b x. S ) ) = ( p ` S ) <-> ( a + ( b x. S ) ) = ( ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) ) ` S ) ) )
19 18 adantl 
 |-  ( ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) /\ p = ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) ) ) -> ( ( a + ( b x. S ) ) = ( p ` S ) <-> ( a + ( b x. S ) ) = ( ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) ) ` S ) ) )
20 simpr 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a e. ZZ /\ b e. ZZ ) )
21 simpl 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> S e. CC )
22 14 11 linply2cfv 
 |-  ( ( ZZ C_ CC /\ ( a e. ZZ /\ b e. ZZ ) /\ S e. CC ) -> ( ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) ) ` S ) = ( a + ( b x. S ) ) )
23 3 20 21 22 mp3an2i 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) ) ` S ) = ( a + ( b x. S ) ) )
24 23 eqcomd 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a + ( b x. S ) ) = ( ( c e. CC |-> sum_ i e. ( 0 ... 1 ) ( ( ( x e. NN0 |-> if ( x = 0 , a , b ) ) ` i ) x. ( c ^ i ) ) ) ` S ) )
25 16 19 24 rspcedvd 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> E. p e. ( Poly ` ZZ ) ( a + ( b x. S ) ) = ( p ` S ) )
26 zsubrg 
 |-  ZZ e. ( SubRing ` CCfld )
27 26 a1i 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ZZ e. ( SubRing ` CCfld ) )
28 eqidd 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) = ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) )
29 27 21 28 rngunsnply 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( ( a + ( b x. S ) ) e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) <-> E. p e. ( Poly ` ZZ ) ( a + ( b x. S ) ) = ( p ` S ) ) )
30 25 29 mpbird 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a + ( b x. S ) ) e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) )
31 elaz 
 |-  ( S e. CC -> ( ( a + ( b x. S ) ) e. ( Z[] ` S ) <-> ( a + ( b x. S ) ) e. ( ( RingSpan ` CCfld ) ` ( ZZ u. { S } ) ) ) )
32 31 adantr 
 |-  ( ( 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 } ) ) ) )
33 30 32 mpbird 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( a + ( b x. S ) ) e. ( Z[] ` S ) )
34 eleq1 
 |-  ( x = ( a + ( b x. S ) ) -> ( x e. ( Z[] ` S ) <-> ( a + ( b x. S ) ) e. ( Z[] ` S ) ) )
35 33 34 syl5ibrcom 
 |-  ( ( S e. CC /\ ( a e. ZZ /\ b e. ZZ ) ) -> ( x = ( a + ( b x. S ) ) -> x e. ( Z[] ` S ) ) )
36 35 rexlimdvva 
 |-  ( S e. CC -> ( E. a e. ZZ E. b e. ZZ x = ( a + ( b x. S ) ) -> x e. ( Z[] ` S ) ) )
37 2 36 syld 
 |-  ( S e. CC -> ( x e. ( Z[]l ` S ) -> x e. ( Z[] ` S ) ) )
38 37 ssrdv 
 |-  ( S e. CC -> ( Z[]l ` S ) C_ ( Z[] ` S ) )