Definition df-mpaa

Description: Define the minimal polynomial of an algebraic number as the unique monic polynomial which achieves the minimum of degAA . (Contributed by Stefan O'Rear, 25-Nov-2014)

	Ref	Expression
Assertion	df-mpaa	⊢ minPolyAA = ( 𝑥 ∈ 𝔸 ↦ ( ℩ 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝑥 ) ∧ ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝑥 ) ) = 1 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmpaa	⊢ minPolyAA
1		vx	⊢ 𝑥
2		caa	⊢ 𝔸
3		vp	⊢ 𝑝
4		cply	⊢ Poly
5		cq	⊢ ℚ
6	5 4	cfv	⊢ ( Poly ‘ ℚ )
7		cdgr	⊢ deg
8	3	cv	⊢ 𝑝
9	8 7	cfv	⊢ ( deg ‘ 𝑝 )
10		cdgraa	⊢ degAA
11	1	cv	⊢ 𝑥
12	11 10	cfv	⊢ ( degAA ‘ 𝑥 )
13	9 12	wceq	⊢ ( deg ‘ 𝑝 ) = ( degAA ‘ 𝑥 )
14	11 8	cfv	⊢ ( 𝑝 ‘ 𝑥 )
15		cc0	⊢ 0
16	14 15	wceq	⊢ ( 𝑝 ‘ 𝑥 ) = 0
17		ccoe	⊢ coeff
18	8 17	cfv	⊢ ( coeff ‘ 𝑝 )
19	12 18	cfv	⊢ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝑥 ) )
20		c1	⊢ 1
21	19 20	wceq	⊢ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝑥 ) ) = 1
22	13 16 21	w3a	⊢ ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝑥 ) ∧ ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝑥 ) ) = 1 )
23	22 3 6	crio	⊢ ( ℩ 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝑥 ) ∧ ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝑥 ) ) = 1 ) )
24	1 2 23	cmpt	⊢ ( 𝑥 ∈ 𝔸 ↦ ( ℩ 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝑥 ) ∧ ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝑥 ) ) = 1 ) ) )
25	0 24	wceq	⊢ minPolyAA = ( 𝑥 ∈ 𝔸 ↦ ( ℩ 𝑝 ∈ ( Poly ‘ ℚ ) ( ( deg ‘ 𝑝 ) = ( degAA ‘ 𝑥 ) ∧ ( 𝑝 ‘ 𝑥 ) = 0 ∧ ( ( coeff ‘ 𝑝 ) ‘ ( degAA ‘ 𝑥 ) ) = 1 ) ) )