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

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		ply1annig1p.k	⊢ 𝐾 = ( RSpan ‘ 𝑃 )
10		ply1annig1p.g	⊢ 𝐺 = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
11		issdrg	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
12	5 11	sylib	⊢ ( 𝜑 → ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
13	12	simp3d	⊢ ( 𝜑 → ( 𝐸 ↾s 𝐹 ) ∈ DivRing )
14	4	fldcrngd	⊢ ( 𝜑 → 𝐸 ∈ CRing )
15	12	simp2d	⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
16	1 2 3 14 15 6 7 8	ply1annidl	⊢ ( 𝜑 → 𝑄 ∈ ( LIdeal ‘ 𝑃 ) )
17		eqid	⊢ ( LIdeal ‘ 𝑃 ) = ( LIdeal ‘ 𝑃 )
18	2 10 17 9	ig1prsp	⊢ ( ( ( 𝐸 ↾s 𝐹 ) ∈ DivRing ∧ 𝑄 ∈ ( LIdeal ‘ 𝑃 ) ) → 𝑄 = ( 𝐾 ‘ { ( 𝐺 ‘ 𝑄 ) } ) )
19	13 16 18	syl2anc	⊢ ( 𝜑 → 𝑄 = ( 𝐾 ‘ { ( 𝐺 ‘ 𝑄 ) } ) )