This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem minplymindeg

Description: The minimal polynomial of A is minimal among the nonzero annihilators of A with regard to degree. (Contributed by Thierry Arnoux, 22-Jun-2025)

Ref Expression
Hypotheses ply1annig1p.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
ply1annig1p.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
ply1annig1p.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
ply1annig1p.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
ply1annig1p.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
ply1annig1p.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
minplymindeg.0 ⊢ 0 = ( 0g ‘ 𝐸 )
minplymindeg.m ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
minplymindeg.d ⊢ 𝐷 = ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) )
minplymindeg.z ⊢ 𝑍 = ( 0g ‘ 𝑃 )
minplymindeg.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
minplymindeg.1 ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐻 ) ‘ 𝐴 ) = 0 )
minplymindeg.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑈 )
minplymindeg.2 ⊢ ( 𝜑 → 𝐻 ≠ 𝑍 )
Assertion minplymindeg ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ≤ ( 𝐷 ‘ 𝐻 ) )

Proof

Step Hyp Ref Expression
1 ply1annig1p.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
2 ply1annig1p.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
3 ply1annig1p.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
4 ply1annig1p.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
5 ply1annig1p.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
6 ply1annig1p.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7 minplymindeg.0 ⊢ 0 = ( 0g ‘ 𝐸 )
8 minplymindeg.m ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
9 minplymindeg.d ⊢ 𝐷 = ( deg1 ‘ ( 𝐸 ↾s 𝐹 ) )
10 minplymindeg.z ⊢ 𝑍 = ( 0g ‘ 𝑃 )
11 minplymindeg.u ⊢ 𝑈 = ( Base ‘ 𝑃 )
12 minplymindeg.1 ⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝐻 ) ‘ 𝐴 ) = 0 )
13 minplymindeg.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑈 )
14 minplymindeg.2 ⊢ ( 𝜑 → 𝐻 ≠ 𝑍 )
15 eqid ⊢ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
16 eqid ⊢ ( RSpan ‘ 𝑃 ) = ( RSpan ‘ 𝑃 )
17 eqid ⊢ ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
18 1 2 3 4 5 6 7 15 16 17 8 minplyval ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) )
19 18 fveq2d ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) = ( 𝐷 ‘ ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) ) )
20 eqid ⊢ ( 𝐸 ↾s 𝐹 ) = ( 𝐸 ↾s 𝐹 )
21 20 sdrgdrng ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
22 5 21 syl ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
23 4 fldcrngd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
24 sdrgsubrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
25 5 24 syl ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
26 1 2 3 23 25 6 7 15 ply1annidl ⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ∈ ( LIdeal ‘ 𝑃 ) )
27 fveq2 ⊢ ( 𝑞 = 𝐻 → ( 𝑂 ‘ 𝑞 ) = ( 𝑂 ‘ 𝐻 ) )
28 27 fveq1d ⊢ ( 𝑞 = 𝐻 → ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( ( 𝑂 ‘ 𝐻 ) ‘ 𝐴 ) )
29 28 eqeq1d ⊢ ( 𝑞 = 𝐻 → ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 ↔ ( ( 𝑂 ‘ 𝐻 ) ‘ 𝐴 ) = 0 ) )
30 1 2 11 23 25 evls1dm ⊢ ( 𝜑 → dom 𝑂 = 𝑈 )
31 13 30 eleqtrrd ⊢ ( 𝜑 → 𝐻 ∈ dom 𝑂 )
32 29 31 12 elrabd ⊢ ( 𝜑 → 𝐻 ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
33 2 17 11 22 26 9 10 32 14 ig1pmindeg ⊢ ( 𝜑 → ( 𝐷 ‘ ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) ) ≤ ( 𝐷 ‘ 𝐻 ) )
34 19 33 eqbrtrd ⊢ ( 𝜑 → ( 𝐷 ‘ ( 𝑀 ‘ 𝐴 ) ) ≤ ( 𝐷 ‘ 𝐻 ) )