Metamath Proof Explorer

Theorem ply1annprmidl

Description: The set Q of polynomials annihilating an element A is a prime ideal. (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 ˙
Assertion ply1annprmidl ⊢ φ → Q ∈ PrmIdeal ⁡ 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 4 fldcrngd ⊢ φ → E ∈ CRing
10 issdrg ⊢ F ∈ SubDRing ⁡ E ↔ E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
11 5 10 sylib ⊢ φ → E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
12 11 simp2d ⊢ φ → F ∈ SubRing ⁡ E
13 eqid ⊢ p ∈ Base P ⟼ O ⁡ p ⁡ A = p ∈ Base P ⟼ O ⁡ p ⁡ A
14 1 2 3 9 12 6 7 8 13 ply1annidllem ⊢ φ → Q = p ∈ Base P ⟼ O ⁡ p ⁡ A -1 0 ˙
15 eqid ⊢ Base P = Base P
16 1 2 3 15 9 12 6 13 evls1maprhm ⊢ φ → p ∈ Base P ⟼ O ⁡ p ⁡ A ∈ P RingHom E
17 fldidom ⊢ E ∈ Field → E ∈ IDomn
18 7 prmidl0 ⊢ E ∈ CRing ∧ 0 ˙ ∈ PrmIdeal ⁡ E ↔ E ∈ IDomn
19 18 biimpri ⊢ E ∈ IDomn → E ∈ CRing ∧ 0 ˙ ∈ PrmIdeal ⁡ E
20 4 17 19 3syl ⊢ φ → E ∈ CRing ∧ 0 ˙ ∈ PrmIdeal ⁡ E
21 20 simprd ⊢ φ → 0 ˙ ∈ PrmIdeal ⁡ E
22 eqid ⊢ PrmIdeal ⁡ P = PrmIdeal ⁡ P
23 22 rhmpreimaprmidl ⊢ E ∈ CRing ∧ p ∈ Base P ⟼ O ⁡ p ⁡ A ∈ P RingHom E ∧ 0 ˙ ∈ PrmIdeal ⁡ E → p ∈ Base P ⟼ O ⁡ p ⁡ A -1 0 ˙ ∈ PrmIdeal ⁡ P
24 9 16 21 23 syl21anc ⊢ φ → p ∈ Base P ⟼ O ⁡ p ⁡ A -1 0 ˙ ∈ PrmIdeal ⁡ P
25 14 24 eqeltrd ⊢ φ → Q ∈ PrmIdeal ⁡ P