Metamath Proof Explorer

Theorem minplycl

Description: The minimal polynomial is a polynomial. (Contributed by Thierry Arnoux, 22-Mar-2025)

Ref Expression
Hypotheses ply1annig1p.o ⊢ O = E evalSub 1 F
ply1annig1p.p ⊢ P = Poly 1 ⁡ E ↾ 𝑠 F
ply1annig1p.b ⊢ B = Base E
ply1annig1p.e ⊢ φ → E ∈ Field
ply1annig1p.f ⊢ φ → F ∈ SubDRing ⁡ E
ply1annig1p.a ⊢ φ → A ∈ B
ply1annig1p.0 ⊢ 0 ˙ = 0 E
ply1annig1p.q ⊢ Q = q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
ply1annig1p.k ⊢ K = RSpan ⁡ P
ply1annig1p.g ⊢ G = idlGen 1p ⁡ E ↾ 𝑠 F
minplyval.1 ⊢ M = E minPoly F
Assertion minplycl ⊢ φ → M ⁡ A ∈ Base P

Proof

Step Hyp Ref Expression
1 ply1annig1p.o ⊢ O = E evalSub 1 F
2 ply1annig1p.p ⊢ P = Poly 1 ⁡ E ↾ 𝑠 F
3 ply1annig1p.b ⊢ B = Base E
4 ply1annig1p.e ⊢ φ → E ∈ Field
5 ply1annig1p.f ⊢ φ → F ∈ SubDRing ⁡ E
6 ply1annig1p.a ⊢ φ → A ∈ B
7 ply1annig1p.0 ⊢ 0 ˙ = 0 E
8 ply1annig1p.q ⊢ Q = q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
9 ply1annig1p.k ⊢ K = RSpan ⁡ P
10 ply1annig1p.g ⊢ G = idlGen 1p ⁡ E ↾ 𝑠 F
11 minplyval.1 ⊢ M = E minPoly F
12 1 2 3 4 5 6 7 8 9 10 11 minplyval ⊢ φ → M ⁡ A = G ⁡ Q
13 4 fldcrngd ⊢ φ → E ∈ CRing
14 issdrg ⊢ F ∈ SubDRing ⁡ E ↔ E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
15 5 14 sylib ⊢ φ → E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
16 15 simp2d ⊢ φ → F ∈ SubRing ⁡ E
17 1 2 3 13 16 6 7 8 ply1annidl ⊢ φ → Q ∈ LIdeal ⁡ P
18 eqid ⊢ Base P = Base P
19 eqid ⊢ LIdeal ⁡ P = LIdeal ⁡ P
20 18 19 lidlss ⊢ Q ∈ LIdeal ⁡ P → Q ⊆ Base P
21 17 20 syl ⊢ φ → Q ⊆ Base P
22 15 simp3d ⊢ φ → E ↾ 𝑠 F ∈ DivRing
23 2 10 19 ig1pcl ⊢ E ↾ 𝑠 F ∈ DivRing ∧ Q ∈ LIdeal ⁡ P → G ⁡ Q ∈ Q
24 22 17 23 syl2anc ⊢ φ → G ⁡ Q ∈ Q
25 21 24 sseldd ⊢ φ → G ⁡ Q ∈ Base P
26 12 25 eqeltrd ⊢ φ → M ⁡ A ∈ Base P