Metamath Proof Explorer

Theorem itgocn

Description: All integral elements are complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Assertion itgocn 
|- ( IntgOver ` S ) C_ CC

Proof

Step Hyp Ref Expression
1 df-itgo 
 |-  IntgOver = ( a e. ~P CC |-> { b e. CC | E. c e. ( Poly ` a ) ( ( c ` b ) = 0 /\ ( ( coeff ` c ) ` ( deg ` c ) ) = 1 ) } )
2 1 dmmptss 
 |-  dom IntgOver C_ ~P CC
3 2 sseli 
 |-  ( S e. dom IntgOver -> S e. ~P CC )
4 cnex 
 |-  CC e. _V
5 4 elpw2 
 |-  ( S e. ~P CC <-> S C_ CC )
6 itgoval 
 |-  ( S C_ CC -> ( IntgOver ` S ) = { a e. CC | E. b e. ( Poly ` S ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } )
7 ssrab2 
 |-  { a e. CC | E. b e. ( Poly ` S ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } C_ CC
8 6 7 eqsstrdi 
 |-  ( S C_ CC -> ( IntgOver ` S ) C_ CC )
9 5 8 sylbi 
 |-  ( S e. ~P CC -> ( IntgOver ` S ) C_ CC )
10 3 9 syl 
 |-  ( S e. dom IntgOver -> ( IntgOver ` S ) C_ CC )
11 ndmfv 
 |-  ( -. S e. dom IntgOver -> ( IntgOver ` S ) = (/) )
12 0ss 
 |-  (/) C_ CC
13 11 12 eqsstrdi 
 |-  ( -. S e. dom IntgOver -> ( IntgOver ` S ) C_ CC )
14 10 13 pm2.61i 
 |-  ( IntgOver ` S ) C_ CC