ply1annidllem

Description: Write the set Q of polynomials annihilating an element A as the kernel of the ring homomorphism F mapping polynomials p to their subring evaluation at a given point A . (Contributed by Thierry Arnoux, 9-Feb-2025)

	Ref	Expression
Hypotheses	ply1annidl.o	⊢ 𝑂 = ( 𝑅 evalSub₁ 𝑆 )
	ply1annidl.p	⊢ 𝑃 = ( Poly₁ ‘ ( 𝑅 ↾_s 𝑆 ) )
	ply1annidl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	ply1annidl.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	ply1annidl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
	ply1annidl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	ply1annidl.0	⊢ 0 = ( 0_g ‘ 𝑅 )
	ply1annidl.q	⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
	ply1annidllem.f	⊢ 𝐹 = ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
Assertion	ply1annidllem	⊢ ( 𝜑 → 𝑄 = ( ^◡ 𝐹 “ { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		ply1annidl.o	⊢ 𝑂 = ( 𝑅 evalSub₁ 𝑆 )
2		ply1annidl.p	⊢ 𝑃 = ( Poly₁ ‘ ( 𝑅 ↾_s 𝑆 ) )
3		ply1annidl.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
4		ply1annidl.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
5		ply1annidl.s	⊢ ( 𝜑 → 𝑆 ∈ ( SubRing ‘ 𝑅 ) )
6		ply1annidl.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7		ply1annidl.0	⊢ 0 = ( 0_g ‘ 𝑅 )
8		ply1annidl.q	⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
9		ply1annidllem.f	⊢ 𝐹 = ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
10		nfv	⊢ Ⅎ 𝑝 𝜑
11		fvexd	⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( Base ‘ 𝑃 ) ) → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ∈ V )
12	10 11 9	fnmptd	⊢ ( 𝜑 → 𝐹 Fn ( Base ‘ 𝑃 ) )
13		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
14	1 2 13 4 5	evls1fn	⊢ ( 𝜑 → 𝑂 Fn ( Base ‘ 𝑃 ) )
15	14	fndmd	⊢ ( 𝜑 → dom 𝑂 = ( Base ‘ 𝑃 ) )
16	15	fneq2d	⊢ ( 𝜑 → ( 𝐹 Fn dom 𝑂 ↔ 𝐹 Fn ( Base ‘ 𝑃 ) ) )
17	12 16	mpbird	⊢ ( 𝜑 → 𝐹 Fn dom 𝑂 )
18		fniniseg2	⊢ ( 𝐹 Fn dom 𝑂 → ( ^◡ 𝐹 “ { 0 } ) = { 𝑞 ∈ dom 𝑂 ∣ ( 𝐹 ‘ 𝑞 ) = 0 } )
19	17 18	syl	⊢ ( 𝜑 → ( ^◡ 𝐹 “ { 0 } ) = { 𝑞 ∈ dom 𝑂 ∣ ( 𝐹 ‘ 𝑞 ) = 0 } )
20		fveq2	⊢ ( 𝑝 = 𝑞 → ( 𝑂 ‘ 𝑝 ) = ( 𝑂 ‘ 𝑞 ) )
21	20	fveq1d	⊢ ( 𝑝 = 𝑞 → ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) = ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) )
22	15	eleq2d	⊢ ( 𝜑 → ( 𝑞 ∈ dom 𝑂 ↔ 𝑞 ∈ ( Base ‘ 𝑃 ) ) )
23	22	biimpa	⊢ ( ( 𝜑 ∧ 𝑞 ∈ dom 𝑂 ) → 𝑞 ∈ ( Base ‘ 𝑃 ) )
24		fvexd	⊢ ( ( 𝜑 ∧ 𝑞 ∈ dom 𝑂 ) → ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) ∈ V )
25	9 21 23 24	fvmptd3	⊢ ( ( 𝜑 ∧ 𝑞 ∈ dom 𝑂 ) → ( 𝐹 ‘ 𝑞 ) = ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) )
26	25	eqeq1d	⊢ ( ( 𝜑 ∧ 𝑞 ∈ dom 𝑂 ) → ( ( 𝐹 ‘ 𝑞 ) = 0 ↔ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 ) )
27	26	rabbidva	⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( 𝐹 ‘ 𝑞 ) = 0 } = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } )
28	19 27	eqtr2d	⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 } = ( ^◡ 𝐹 “ { 0 } ) )
29	8 28	eqtrid	⊢ ( 𝜑 → 𝑄 = ( ^◡ 𝐹 “ { 0 } ) )

Metamath Proof Explorer

Theorem ply1annidllem

Proof