Metamath Proof Explorer

Theorem aaitgo

Description: The standard algebraic numbers AA are generated by IntgOver . (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Assertion aaitgo 
|- AA = ( IntgOver ` QQ )

Proof

Step Hyp Ref Expression
1 rabid 
 |-  ( a e. { a e. CC | E. b e. ( Poly ` QQ ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } <-> ( a e. CC /\ E. b e. ( Poly ` QQ ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) )
2 qsscn 
 |-  QQ C_ CC
3 itgoval 
 |-  ( QQ C_ CC -> ( IntgOver ` QQ ) = { a e. CC | E. b e. ( Poly ` QQ ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } )
4 2 3 ax-mp 
 |-  ( IntgOver ` QQ ) = { a e. CC | E. b e. ( Poly ` QQ ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) }
5 4 eleq2i 
 |-  ( a e. ( IntgOver ` QQ ) <-> a e. { a e. CC | E. b e. ( Poly ` QQ ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) } )
6 aacn 
 |-  ( a e. AA -> a e. CC )
7 mpaacl 
 |-  ( a e. AA -> ( minPolyAA ` a ) e. ( Poly ` QQ ) )
8 mpaaroot 
 |-  ( a e. AA -> ( ( minPolyAA ` a ) ` a ) = 0 )
9 mpaadgr 
 |-  ( a e. AA -> ( deg ` ( minPolyAA ` a ) ) = ( degAA ` a ) )
10 9 fveq2d 
 |-  ( a e. AA -> ( ( coeff ` ( minPolyAA ` a ) ) ` ( deg ` ( minPolyAA ` a ) ) ) = ( ( coeff ` ( minPolyAA ` a ) ) ` ( degAA ` a ) ) )
11 mpaamn 
 |-  ( a e. AA -> ( ( coeff ` ( minPolyAA ` a ) ) ` ( degAA ` a ) ) = 1 )
12 10 11 eqtrd 
 |-  ( a e. AA -> ( ( coeff ` ( minPolyAA ` a ) ) ` ( deg ` ( minPolyAA ` a ) ) ) = 1 )
13 fveq1 
 |-  ( b = ( minPolyAA ` a ) -> ( b ` a ) = ( ( minPolyAA ` a ) ` a ) )
14 13 eqeq1d 
 |-  ( b = ( minPolyAA ` a ) -> ( ( b ` a ) = 0 <-> ( ( minPolyAA ` a ) ` a ) = 0 ) )
15 fveq2 
 |-  ( b = ( minPolyAA ` a ) -> ( coeff ` b ) = ( coeff ` ( minPolyAA ` a ) ) )
16 fveq2 
 |-  ( b = ( minPolyAA ` a ) -> ( deg ` b ) = ( deg ` ( minPolyAA ` a ) ) )
17 15 16 fveq12d 
 |-  ( b = ( minPolyAA ` a ) -> ( ( coeff ` b ) ` ( deg ` b ) ) = ( ( coeff ` ( minPolyAA ` a ) ) ` ( deg ` ( minPolyAA ` a ) ) ) )
18 17 eqeq1d 
 |-  ( b = ( minPolyAA ` a ) -> ( ( ( coeff ` b ) ` ( deg ` b ) ) = 1 <-> ( ( coeff ` ( minPolyAA ` a ) ) ` ( deg ` ( minPolyAA ` a ) ) ) = 1 ) )
19 14 18 anbi12d 
 |-  ( b = ( minPolyAA ` a ) -> ( ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) <-> ( ( ( minPolyAA ` a ) ` a ) = 0 /\ ( ( coeff ` ( minPolyAA ` a ) ) ` ( deg ` ( minPolyAA ` a ) ) ) = 1 ) ) )
20 19 rspcev 
 |-  ( ( ( minPolyAA ` a ) e. ( Poly ` QQ ) /\ ( ( ( minPolyAA ` a ) ` a ) = 0 /\ ( ( coeff ` ( minPolyAA ` a ) ) ` ( deg ` ( minPolyAA ` a ) ) ) = 1 ) ) -> E. b e. ( Poly ` QQ ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) )
21 7 8 12 20 syl12anc 
 |-  ( a e. AA -> E. b e. ( Poly ` QQ ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) )
22 6 21 jca 
 |-  ( a e. AA -> ( a e. CC /\ E. b e. ( Poly ` QQ ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) )
23 simpl 
 |-  ( ( b e. ( Poly ` QQ ) /\ ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) -> b e. ( Poly ` QQ ) )
24 coe0 
 |-  ( coeff ` 0p ) = ( NN0 X. { 0 } )
25 24 fveq1i 
 |-  ( ( coeff ` 0p ) ` ( deg ` 0p ) ) = ( ( NN0 X. { 0 } ) ` ( deg ` 0p ) )
26 dgr0 
 |-  ( deg ` 0p ) = 0
27 0nn0 
 |-  0 e. NN0
28 26 27 eqeltri 
 |-  ( deg ` 0p ) e. NN0
29 c0ex 
 |-  0 e. _V
30 29 fvconst2 
 |-  ( ( deg ` 0p ) e. NN0 -> ( ( NN0 X. { 0 } ) ` ( deg ` 0p ) ) = 0 )
31 28 30 ax-mp 
 |-  ( ( NN0 X. { 0 } ) ` ( deg ` 0p ) ) = 0
32 25 31 eqtri 
 |-  ( ( coeff ` 0p ) ` ( deg ` 0p ) ) = 0
33 0ne1 
 |-  0 =/= 1
34 32 33 eqnetri 
 |-  ( ( coeff ` 0p ) ` ( deg ` 0p ) ) =/= 1
35 fveq2 
 |-  ( b = 0p -> ( coeff ` b ) = ( coeff ` 0p ) )
36 fveq2 
 |-  ( b = 0p -> ( deg ` b ) = ( deg ` 0p ) )
37 35 36 fveq12d 
 |-  ( b = 0p -> ( ( coeff ` b ) ` ( deg ` b ) ) = ( ( coeff ` 0p ) ` ( deg ` 0p ) ) )
38 37 neeq1d 
 |-  ( b = 0p -> ( ( ( coeff ` b ) ` ( deg ` b ) ) =/= 1 <-> ( ( coeff ` 0p ) ` ( deg ` 0p ) ) =/= 1 ) )
39 34 38 mpbiri 
 |-  ( b = 0p -> ( ( coeff ` b ) ` ( deg ` b ) ) =/= 1 )
40 39 necon2i 
 |-  ( ( ( coeff ` b ) ` ( deg ` b ) ) = 1 -> b =/= 0p )
41 40 ad2antll 
 |-  ( ( b e. ( Poly ` QQ ) /\ ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) -> b =/= 0p )
42 eldifsn 
 |-  ( b e. ( ( Poly ` QQ ) \ { 0p } ) <-> ( b e. ( Poly ` QQ ) /\ b =/= 0p ) )
43 23 41 42 sylanbrc 
 |-  ( ( b e. ( Poly ` QQ ) /\ ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) -> b e. ( ( Poly ` QQ ) \ { 0p } ) )
44 simprl 
 |-  ( ( b e. ( Poly ` QQ ) /\ ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) -> ( b ` a ) = 0 )
45 43 44 jca 
 |-  ( ( b e. ( Poly ` QQ ) /\ ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) -> ( b e. ( ( Poly ` QQ ) \ { 0p } ) /\ ( b ` a ) = 0 ) )
46 45 reximi2 
 |-  ( E. b e. ( Poly ` QQ ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) -> E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( b ` a ) = 0 )
47 46 anim2i 
 |-  ( ( a e. CC /\ E. b e. ( Poly ` QQ ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) -> ( a e. CC /\ E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( b ` a ) = 0 ) )
48 elqaa 
 |-  ( a e. AA <-> ( a e. CC /\ E. b e. ( ( Poly ` QQ ) \ { 0p } ) ( b ` a ) = 0 ) )
49 47 48 sylibr 
 |-  ( ( a e. CC /\ E. b e. ( Poly ` QQ ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) -> a e. AA )
50 22 49 impbii 
 |-  ( a e. AA <-> ( a e. CC /\ E. b e. ( Poly ` QQ ) ( ( b ` a ) = 0 /\ ( ( coeff ` b ) ` ( deg ` b ) ) = 1 ) ) )
51 1 5 50 3bitr4ri 
 |-  ( a e. AA <-> a e. ( IntgOver ` QQ ) )
52 51 eqriv 
 |-  AA = ( IntgOver ` QQ )