Metamath Proof Explorer

Theorem ply1annig1p

Description: The ideal Q of polynomials annihilating an element A is generated by the ideal's canonical generator. (Contributed by Thierry Arnoux, 9-Feb-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
Assertion ply1annig1p ⊢ φ → Q = K ⁡ G ⁡ Q

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 issdrg ⊢ F ∈ SubDRing ⁡ E ↔ E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
12 5 11 sylib ⊢ φ → E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
13 12 simp3d ⊢ φ → E ↾ 𝑠 F ∈ DivRing
14 4 fldcrngd ⊢ φ → E ∈ CRing
15 12 simp2d ⊢ φ → F ∈ SubRing ⁡ E
16 1 2 3 14 15 6 7 8 ply1annidl ⊢ φ → Q ∈ LIdeal ⁡ P
17 eqid ⊢ LIdeal ⁡ P = LIdeal ⁡ P
18 2 10 17 9 ig1prsp ⊢ E ↾ 𝑠 F ∈ DivRing ∧ Q ∈ LIdeal ⁡ P → Q = K ⁡ G ⁡ Q
19 13 16 18 syl2anc ⊢ φ → Q = K ⁡ G ⁡ Q