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	⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
	ply1annig1p.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
	ply1annig1p.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
	ply1annig1p.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
	ply1annig1p.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	ply1annig1p.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	ply1annig1p.0	⊢ 0 = ( 0g ‘ 𝐸 )
	ply1annig1p.q	⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
Assertion	ply1annprmidl	⊢ ( 𝜑 → 𝑄 ∈ ( PrmIdeal ‘ 𝑃 ) )

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		ply1annig1p.0	⊢ 0 = ( 0g ‘ 𝐸 )
8		ply1annig1p.q	⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
9	4	fldcrngd	⊢ ( 𝜑 → 𝐸 ∈ CRing )
10		issdrg	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
11	5 10	sylib	⊢ ( 𝜑 → ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
12	11	simp2d	⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
13		eqid	⊢ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) = ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
14	1 2 3 9 12 6 7 8 13	ply1annidllem	⊢ ( 𝜑 → 𝑄 = ( ◡ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) “ { 0 } ) )
15		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
16	1 2 3 15 9 12 6 13	evls1maprhm	⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) ∈ ( 𝑃 RingHom 𝐸 ) )
17		fldidom	⊢ ( 𝐸 ∈ Field → 𝐸 ∈ IDomn )
18	7	prmidl0	⊢ ( ( 𝐸 ∈ CRing ∧ { 0 } ∈ ( PrmIdeal ‘ 𝐸 ) ) ↔ 𝐸 ∈ IDomn )
19	18	biimpri	⊢ ( 𝐸 ∈ IDomn → ( 𝐸 ∈ CRing ∧ { 0 } ∈ ( PrmIdeal ‘ 𝐸 ) ) )
20	4 17 19	3syl	⊢ ( 𝜑 → ( 𝐸 ∈ CRing ∧ { 0 } ∈ ( PrmIdeal ‘ 𝐸 ) ) )
21	20	simprd	⊢ ( 𝜑 → { 0 } ∈ ( PrmIdeal ‘ 𝐸 ) )
22		eqid	⊢ ( PrmIdeal ‘ 𝑃 ) = ( PrmIdeal ‘ 𝑃 )
23	22	rhmpreimaprmidl	⊢ ( ( ( 𝐸 ∈ CRing ∧ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) ∈ ( 𝑃 RingHom 𝐸 ) ) ∧ { 0 } ∈ ( PrmIdeal ‘ 𝐸 ) ) → ( ◡ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) “ { 0 } ) ∈ ( PrmIdeal ‘ 𝑃 ) )
24	9 16 21 23	syl21anc	⊢ ( 𝜑 → ( ◡ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) “ { 0 } ) ∈ ( PrmIdeal ‘ 𝑃 ) )
25	14 24	eqeltrd	⊢ ( 𝜑 → 𝑄 ∈ ( PrmIdeal ‘ 𝑃 ) )