Theorem ply1annidl

Description: The set Q of polynomials annihilating an element A forms an ideal. (Contributed by Thierry Arnoux, 9-Feb-2025)

	Ref	Expression
Hypotheses	ply1annidl.o	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
	ply1annidl.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
	ply1annidl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ply1annidl.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	ply1annidl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
	ply1annidl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	ply1annidl.0	⊢ 0 = ( 0g ‘ 𝑅 )
	ply1annidl.q	⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
Assertion	ply1annidl	⊢ ( 𝜑 → 𝑄 ∈ ( LIdeal ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1annidl.o	⊢ 𝑂 = ( 𝑅 evalSub1 𝑆 )
2		ply1annidl.p	⊢ 𝑃 = ( Poly1 ‘ ( 𝑅 ↾s 𝑆 ) )
3		ply1annidl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		ply1annidl.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
5		ply1annidl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
6		ply1annidl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7		ply1annidl.0	⊢ 0 = ( 0g ‘ 𝑅 )
8		ply1annidl.q	⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
9		eqid	⊢ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) = ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
10	1 2 3 4 5 6 7 8 9	ply1annidllem	⊢ ( 𝜑 → 𝑄 = ( ◡ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) “ { 0 } ) )
11		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
12	1 2 3 11 4 5 6 9	evls1maprhm	⊢ ( 𝜑 → ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) ∈ ( 𝑃 RingHom 𝑅 ) )
13	4	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
14		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
15	14 7	lidl0	⊢ ( 𝑅 ∈ Ring → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
16	13 15	syl	⊢ ( 𝜑 → { 0 } ∈ ( LIdeal ‘ 𝑅 ) )
17		eqid	⊢ ( LIdeal ‘ 𝑃 ) = ( LIdeal ‘ 𝑃 )
18	17	rhmpreimaidl	⊢ ( ( ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) ∈ ( 𝑃 RingHom 𝑅 ) ∧ { 0 } ∈ ( LIdeal ‘ 𝑅 ) ) → ( ◡ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) “ { 0 } ) ∈ ( LIdeal ‘ 𝑃 ) )
19	12 16 18	syl2anc	⊢ ( 𝜑 → ( ◡ ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) “ { 0 } ) ∈ ( LIdeal ‘ 𝑃 ) )
20	10 19	eqeltrd	⊢ ( 𝜑 → 𝑄 ∈ ( LIdeal ‘ 𝑃 ) )