minplycl

Description: The minimal polynomial is a polynomial. (Contributed by Thierry Arnoux, 22-Mar-2025)

	Ref	Expression
Hypotheses	ply1annig1p.o	⊢ 𝑂 = ( 𝐸 evalSub₁ 𝐹 )
	ply1annig1p.p	⊢ 𝑃 = ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) )
	ply1annig1p.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
	ply1annig1p.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
	ply1annig1p.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	ply1annig1p.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	ply1annig1p.0	⊢ 0 = ( 0_g ‘ 𝐸 )
	ply1annig1p.q	⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
	ply1annig1p.k	⊢ 𝐾 = ( RSpan ‘ 𝑃 )
	ply1annig1p.g	⊢ 𝐺 = ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) )
	minplyval.1	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
Assertion	minplycl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		ply1annig1p.o	⊢ 𝑂 = ( 𝐸 evalSub₁ 𝐹 )
2		ply1annig1p.p	⊢ 𝑃 = ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) )
3		ply1annig1p.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
4		ply1annig1p.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
5		ply1annig1p.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
6		ply1annig1p.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7		ply1annig1p.0	⊢ 0 = ( 0_g ‘ 𝐸 )
8		ply1annig1p.q	⊢ 𝑄 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = 0 }
9		ply1annig1p.k	⊢ 𝐾 = ( RSpan ‘ 𝑃 )
10		ply1annig1p.g	⊢ 𝐺 = ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) )
11		minplyval.1	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
12	1 2 3 4 5 6 7 8 9 10 11	minplyval	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑄 ) )
13	4	fldcrngd	⊢ ( 𝜑 → 𝐸 ∈ CRing )
14		issdrg	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾_s 𝐹 ) ∈ DivRing ) )
15	5 14	sylib	⊢ ( 𝜑 → ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾_s 𝐹 ) ∈ DivRing ) )
16	15	simp2d	⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
17	1 2 3 13 16 6 7 8	ply1annidl	⊢ ( 𝜑 → 𝑄 ∈ ( LIdeal ‘ 𝑃 ) )
18		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
19		eqid	⊢ ( LIdeal ‘ 𝑃 ) = ( LIdeal ‘ 𝑃 )
20	18 19	lidlss	⊢ ( 𝑄 ∈ ( LIdeal ‘ 𝑃 ) → 𝑄 ⊆ ( Base ‘ 𝑃 ) )
21	17 20	syl	⊢ ( 𝜑 → 𝑄 ⊆ ( Base ‘ 𝑃 ) )
22	15	simp3d	⊢ ( 𝜑 → ( 𝐸 ↾_s 𝐹 ) ∈ DivRing )
23	2 10 19	ig1pcl	⊢ ( ( ( 𝐸 ↾_s 𝐹 ) ∈ DivRing ∧ 𝑄 ∈ ( LIdeal ‘ 𝑃 ) ) → ( 𝐺 ‘ 𝑄 ) ∈ 𝑄 )
24	22 17 23	syl2anc	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑄 ) ∈ 𝑄 )
25	21 24	sseldd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑄 ) ∈ ( Base ‘ 𝑃 ) )
26	12 25	eqeltrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ 𝑃 ) )

Metamath Proof Explorer

Theorem minplycl

Proof