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 ⊢ 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
minplyann.1 ⊢ 0 ˙ = 0 E
minplyann.m ⊢ M = E minPoly F
Assertion minplyann ⊢ φ → O ⁡ M ⁡ A ⁡ A = 0 ˙

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 minplyann.1 ⊢ 0 ˙ = 0 E
8 minplyann.m ⊢ M = E minPoly F
9 eqid ⊢ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙ = q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
10 eqid ⊢ RSpan ⁡ P = RSpan ⁡ P
11 eqid ⊢ idlGen 1p ⁡ E ↾ 𝑠 F = idlGen 1p ⁡ E ↾ 𝑠 F
12 1 2 3 4 5 6 7 9 10 11 8 minplyval ⊢ φ → M ⁡ A = idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
13 eqid ⊢ E ↾ 𝑠 F = E ↾ 𝑠 F
14 13 sdrgdrng ⊢ F ∈ SubDRing ⁡ E → E ↾ 𝑠 F ∈ DivRing
15 5 14 syl ⊢ φ → E ↾ 𝑠 F ∈ DivRing
16 4 fldcrngd ⊢ φ → E ∈ CRing
17 sdrgsubrg ⊢ F ∈ SubDRing ⁡ E → F ∈ SubRing ⁡ E
18 5 17 syl ⊢ φ → F ∈ SubRing ⁡ E
19 1 2 3 16 18 6 7 9 ply1annidl ⊢ φ → q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙ ∈ LIdeal ⁡ P
20 eqid ⊢ LIdeal ⁡ P = LIdeal ⁡ P
21 2 11 20 ig1pcl ⊢ E ↾ 𝑠 F ∈ DivRing ∧ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙ ∈ LIdeal ⁡ P → idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙ ∈ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
22 15 19 21 syl2anc ⊢ φ → idlGen 1p ⁡ E ↾ 𝑠 F ⁡ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙ ∈ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
23 12 22 eqeltrd ⊢ φ → M ⁡ A ∈ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙
24 fveq2 ⊢ q = M ⁡ A → O ⁡ q = O ⁡ M ⁡ A
25 24 fveq1d ⊢ q = M ⁡ A → O ⁡ q ⁡ A = O ⁡ M ⁡ A ⁡ A
26 25 eqeq1d ⊢ q = M ⁡ A → O ⁡ q ⁡ A = 0 ˙ ↔ O ⁡ M ⁡ A ⁡ A = 0 ˙
27 26 elrab ⊢ M ⁡ A ∈ q ∈ dom ⁡ O | O ⁡ q ⁡ A = 0 ˙ ↔ M ⁡ A ∈ dom ⁡ O ∧ O ⁡ M ⁡ A ⁡ A = 0 ˙
28 23 27 sylib ⊢ φ → M ⁡ A ∈ dom ⁡ O ∧ O ⁡ M ⁡ A ⁡ A = 0 ˙
29 28 simprd ⊢ φ → O ⁡ M ⁡ A ⁡ A = 0 ˙