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