Theorem dgraaval

Description: Value of the degree function on an algebraic number. (Contributed by Stefan O'Rear, 25-Nov-2014) (Revised by AV, 29-Sep-2020)

	Ref	Expression
Assertion	dgraaval	⊢ ( 𝐴 ∈ 𝔸 → ( degAA ‘ 𝐴 ) = inf ( { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝐴 ) = 0 ) } , ℝ , < ) )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	⊢ ( 𝑎 = 𝐴 → ( ( 𝑝 ‘ 𝑎 ) = 0 ↔ ( 𝑝 ‘ 𝐴 ) = 0 ) )
2	1	anbi2d	⊢ ( 𝑎 = 𝐴 → ( ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝑎 ) = 0 ) ↔ ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝐴 ) = 0 ) ) )
3	2	rexbidv	⊢ ( 𝑎 = 𝐴 → ( ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝑎 ) = 0 ) ↔ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝐴 ) = 0 ) ) )
4	3	rabbidv	⊢ ( 𝑎 = 𝐴 → { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝑎 ) = 0 ) } = { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝐴 ) = 0 ) } )
5	4	infeq1d	⊢ ( 𝑎 = 𝐴 → inf ( { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝑎 ) = 0 ) } , ℝ , < ) = inf ( { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝐴 ) = 0 ) } , ℝ , < ) )
6		df-dgraa	⊢ degAA = ( 𝑎 ∈ 𝔸 ↦ inf ( { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝑎 ) = 0 ) } , ℝ , < ) )
7		ltso	⊢ < Or ℝ
8	7	infex	⊢ inf ( { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝐴 ) = 0 ) } , ℝ , < ) ∈ V
9	5 6 8	fvmpt	⊢ ( 𝐴 ∈ 𝔸 → ( degAA ‘ 𝐴 ) = inf ( { 𝑑 ∈ ℕ ∣ ∃ 𝑝 ∈ ( ( Poly ‘ ℚ ) ∖ { 0𝑝 } ) ( ( deg ‘ 𝑝 ) = 𝑑 ∧ ( 𝑝 ‘ 𝐴 ) = 0 ) } , ℝ , < ) )