Metamath Proof Explorer


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 ) } , ℝ , < ) )