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

Metamath Proof Explorer

Theorem minplyann

Description: The minimal polynomial for A annihilates A . (Contributed by Thierry Arnoux, 25-Apr-2025)

Ref Expression
Hypotheses ply1annig1p.o ⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
ply1annig1p.p ⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
ply1annig1p.b ⊢ 𝐵 = ( Base ‘ 𝐸 )
ply1annig1p.e ⊢ ( 𝜑 → 𝐸 ∈ Field )
ply1annig1p.f ⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
ply1annig1p.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
minplyann.1 ⊢ 0 = ( 0g ‘ 𝐸 )
minplyann.m ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
Assertion minplyann ( 𝜑 → ( ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) = 0 )

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 minplyann.1 ⊢ 0 = ( 0g ‘ 𝐸 )
8 minplyann.m ⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
9 eqid ⊢ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
10 eqid ⊢ ( RSpan ‘ 𝑃 ) = ( RSpan ‘ 𝑃 )
11 eqid ⊢ ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
12 1 2 3 4 5 6 7 9 10 11 8 minplyval ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) )
13 eqid ⊢ ( 𝐸 ↾s 𝐹 ) = ( 𝐸 ↾s 𝐹 )
14 13 sdrgdrng ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
15 5 14 syl ⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
16 4 fldcrngd ⊢ ( 𝜑 → 𝐸 ∈ CRing )
17 sdrgsubrg ⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
18 5 17 syl ⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
19 1 2 3 16 18 6 7 9 ply1annidl ⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ∈ ( LIdeal ‘ 𝑃 ) )
20 eqid ⊢ ( LIdeal ‘ 𝑃 ) = ( LIdeal ‘ 𝑃 )
21 2 11 20 ig1pcl ⊢ ( ( ( 𝐸 ↾s 𝐹 ) ∈ DivRing ∧ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ∈ ( LIdeal ‘ 𝑃 ) ) → ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
22 15 19 21 syl2anc ⊢ ( 𝜑 → ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
23 12 22 eqeltrd ⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
24 fveq2 ⊢ ( 𝑞 = ( 𝑀 ‘ 𝐴 ) → ( 𝑂 ‘ 𝑞 ) = ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) )
25 24 fveq1d ⊢ ( 𝑞 = ( 𝑀 ‘ 𝐴 ) → ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) )
26 25 eqeq1d ⊢ ( 𝑞 = ( 𝑀 ‘ 𝐴 ) → ( ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 ↔ ( ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) = 0 ) )
27 26 elrab ⊢ ( ( 𝑀 ‘ 𝐴 ) ∈ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } ↔ ( ( 𝑀 ‘ 𝐴 ) ∈ dom 𝑂 ∧ ( ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) = 0 ) )
28 23 27 sylib ⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) ∈ dom 𝑂 ∧ ( ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) = 0 ) )
29 28 simprd ⊢ ( 𝜑 → ( ( 𝑂 ‘ ( 𝑀 ‘ 𝐴 ) ) ‘ 𝐴 ) = 0 )