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 𝔸 = ( IntgOver ‘ ℚ )

Proof

Step Hyp Ref Expression
1 rabid ⊢ ( 𝑎 ∈ { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ ℚ ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } ↔ ( 𝑎 ∈ ℂ ∧ ∃ 𝑏 ∈ ( Poly ‘ ℚ ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) )
2 qsscn ⊢ ℚ ⊆ ℂ
3 itgoval ⊢ ( ℚ ⊆ ℂ → ( IntgOver ‘ ℚ ) = { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ ℚ ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
4 2 3 ax-mp ⊢ ( IntgOver ‘ ℚ ) = { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ ℚ ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) }
5 4 eleq2i ⊢ ( 𝑎 ∈ ( IntgOver ‘ ℚ ) ↔ 𝑎 ∈ { 𝑎 ∈ ℂ ∣ ∃ 𝑏 ∈ ( Poly ‘ ℚ ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) } )
6 aacn ⊢ ( 𝑎 ∈ 𝔸 → 𝑎 ∈ ℂ )
7 mpaacl ⊢ ( 𝑎 ∈ 𝔸 → ( minPolyAA ‘ 𝑎 ) ∈ ( Poly ‘ ℚ ) )
8 mpaaroot ⊢ ( 𝑎 ∈ 𝔸 → ( ( minPolyAA ‘ 𝑎 ) ‘ 𝑎 ) = 0 )
9 mpaadgr ⊢ ( 𝑎 ∈ 𝔸 → ( deg ‘ ( minPolyAA ‘ 𝑎 ) ) = ( degAA ‘ 𝑎 ) )
10 9 fveq2d ⊢ ( 𝑎 ∈ 𝔸 → ( ( coeff ‘ ( minPolyAA ‘ 𝑎 ) ) ‘ ( deg ‘ ( minPolyAA ‘ 𝑎 ) ) ) = ( ( coeff ‘ ( minPolyAA ‘ 𝑎 ) ) ‘ ( degAA ‘ 𝑎 ) ) )
11 mpaamn ⊢ ( 𝑎 ∈ 𝔸 → ( ( coeff ‘ ( minPolyAA ‘ 𝑎 ) ) ‘ ( degAA ‘ 𝑎 ) ) = 1 )
12 10 11 eqtrd ⊢ ( 𝑎 ∈ 𝔸 → ( ( coeff ‘ ( minPolyAA ‘ 𝑎 ) ) ‘ ( deg ‘ ( minPolyAA ‘ 𝑎 ) ) ) = 1 )
13 fveq1 ⊢ ( 𝑏 = ( minPolyAA ‘ 𝑎 ) → ( 𝑏 ‘ 𝑎 ) = ( ( minPolyAA ‘ 𝑎 ) ‘ 𝑎 ) )
14 13 eqeq1d ⊢ ( 𝑏 = ( minPolyAA ‘ 𝑎 ) → ( ( 𝑏 ‘ 𝑎 ) = 0 ↔ ( ( minPolyAA ‘ 𝑎 ) ‘ 𝑎 ) = 0 ) )
15 fveq2 ⊢ ( 𝑏 = ( minPolyAA ‘ 𝑎 ) → ( coeff ‘ 𝑏 ) = ( coeff ‘ ( minPolyAA ‘ 𝑎 ) ) )
16 fveq2 ⊢ ( 𝑏 = ( minPolyAA ‘ 𝑎 ) → ( deg ‘ 𝑏 ) = ( deg ‘ ( minPolyAA ‘ 𝑎 ) ) )
17 15 16 fveq12d ⊢ ( 𝑏 = ( minPolyAA ‘ 𝑎 ) → ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = ( ( coeff ‘ ( minPolyAA ‘ 𝑎 ) ) ‘ ( deg ‘ ( minPolyAA ‘ 𝑎 ) ) ) )
18 17 eqeq1d ⊢ ( 𝑏 = ( minPolyAA ‘ 𝑎 ) → ( ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ↔ ( ( coeff ‘ ( minPolyAA ‘ 𝑎 ) ) ‘ ( deg ‘ ( minPolyAA ‘ 𝑎 ) ) ) = 1 ) )
19 14 18 anbi12d ⊢ ( 𝑏 = ( minPolyAA ‘ 𝑎 ) → ( ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ↔ ( ( ( minPolyAA ‘ 𝑎 ) ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ ( minPolyAA ‘ 𝑎 ) ) ‘ ( deg ‘ ( minPolyAA ‘ 𝑎 ) ) ) = 1 ) ) )
20 19 rspcev ⊢ ( ( ( minPolyAA ‘ 𝑎 ) ∈ ( Poly ‘ ℚ ) ∧ ( ( ( minPolyAA ‘ 𝑎 ) ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ ( minPolyAA ‘ 𝑎 ) ) ‘ ( deg ‘ ( minPolyAA ‘ 𝑎 ) ) ) = 1 ) ) → ∃ 𝑏 ∈ ( Poly ‘ ℚ ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) )
21 7 8 12 20 syl12anc ⊢ ( 𝑎 ∈ 𝔸 → ∃ 𝑏 ∈ ( Poly ‘ ℚ ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) )
22 6 21 jca ⊢ ( 𝑎 ∈ 𝔸 → ( 𝑎 ∈ ℂ ∧ ∃ 𝑏 ∈ ( Poly ‘ ℚ ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) )
23 simpl ⊢ ( ( 𝑏 ∈ ( Poly ‘ ℚ ) ∧ ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) → 𝑏 ∈ ( Poly ‘ ℚ ) )
24 coe0 ⊢ ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } )
25 24 fveq1i ⊢ ( ( coeff ‘ 0𝑝 ) ‘ ( deg ‘ 0𝑝 ) ) = ( ( ℕ0 × { 0 } ) ‘ ( deg ‘ 0𝑝 ) )
26 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
27 0nn0 ⊢ 0 ∈ ℕ0
28 26 27 eqeltri ⊢ ( deg ‘ 0𝑝 ) ∈ ℕ0
29 c0ex ⊢ 0 ∈ V
30 29 fvconst2 ⊢ ( ( deg ‘ 0𝑝 ) ∈ ℕ0 → ( ( ℕ0 × { 0 } ) ‘ ( deg ‘ 0𝑝 ) ) = 0 )
31 28 30 ax-mp ⊢ ( ( ℕ0 × { 0 } ) ‘ ( deg ‘ 0𝑝 ) ) = 0
32 25 31 eqtri ⊢ ( ( coeff ‘ 0𝑝 ) ‘ ( deg ‘ 0𝑝 ) ) = 0
33 0ne1 ⊢ 0 ≠ 1
34 32 33 eqnetri ⊢ ( ( coeff ‘ 0𝑝 ) ‘ ( deg ‘ 0𝑝 ) ) ≠ 1
35 fveq2 ⊢ ( 𝑏 = 0𝑝 → ( coeff ‘ 𝑏 ) = ( coeff ‘ 0𝑝 ) )
36 fveq2 ⊢ ( 𝑏 = 0𝑝 → ( deg ‘ 𝑏 ) = ( deg ‘ 0𝑝 ) )
37 35 36 fveq12d ⊢ ( 𝑏 = 0𝑝 → ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = ( ( coeff ‘ 0𝑝 ) ‘ ( deg ‘ 0𝑝 ) ) )
38 37 neeq1d ⊢ ( 𝑏 = 0𝑝 → ( ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) ≠ 1 ↔ ( ( coeff ‘ 0𝑝 ) ‘ ( deg ‘ 0𝑝 ) ) ≠ 1 ) )
39 34 38 mpbiri ⊢ ( 𝑏 = 0𝑝 → ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) ≠ 1 )
40 39 necon2i ⊢ ( ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 → 𝑏 ≠ 0𝑝 )
41 40 ad2antll ⊢ ( ( 𝑏 ∈ ( Poly ‘ ℚ ) ∧ ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) → 𝑏 ≠ 0𝑝 )
42 eldifsn ⊢ ( 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ↔ ( 𝑏 ∈ ( Poly ‘ ℚ ) ∧ 𝑏 ≠ 0𝑝 ) )
43 23 41 42 sylanbrc ⊢ ( ( 𝑏 ∈ ( Poly ‘ ℚ ) ∧ ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) → 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) )
44 simprl ⊢ ( ( 𝑏 ∈ ( Poly ‘ ℚ ) ∧ ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) → ( 𝑏 ‘ 𝑎 ) = 0 )
45 43 44 jca ⊢ ( ( 𝑏 ∈ ( Poly ‘ ℚ ) ∧ ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) → ( 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ∧ ( 𝑏 ‘ 𝑎 ) = 0 ) )
46 45 reximi2 ⊢ ( ∃ 𝑏 ∈ ( Poly ‘ ℚ ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) → ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑏 ‘ 𝑎 ) = 0 )
47 46 anim2i ⊢ ( ( 𝑎 ∈ ℂ ∧ ∃ 𝑏 ∈ ( Poly ‘ ℚ ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) → ( 𝑎 ∈ ℂ ∧ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑏 ‘ 𝑎 ) = 0 ) )
48 elqaa ⊢ ( 𝑎 ∈ 𝔸 ↔ ( 𝑎 ∈ ℂ ∧ ∃ 𝑏 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( 𝑏 ‘ 𝑎 ) = 0 ) )
49 47 48 sylibr ⊢ ( ( 𝑎 ∈ ℂ ∧ ∃ 𝑏 ∈ ( Poly ‘ ℚ ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) → 𝑎 ∈ 𝔸 )
50 22 49 impbii ⊢ ( 𝑎 ∈ 𝔸 ↔ ( 𝑎 ∈ ℂ ∧ ∃ 𝑏 ∈ ( Poly ‘ ℚ ) ( ( 𝑏 ‘ 𝑎 ) = 0 ∧ ( ( coeff ‘ 𝑏 ) ‘ ( deg ‘ 𝑏 ) ) = 1 ) ) )
51 1 5 50 3bitr4ri ⊢ ( 𝑎 ∈ 𝔸 ↔ 𝑎 ∈ ( IntgOver ‘ ℚ ) )
52 51 eqriv ⊢ 𝔸 = ( IntgOver ‘ ℚ )