minplynzm1p

Description: If a minimal polynomial is nonzero, then it is monic. (Contributed by Thierry Arnoux, 26-Oct-2025)

	Ref	Expression
Hypotheses	minplynzm1p.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
	minplynzm1p.z	⊢ 𝑍 = ( 0_g ‘ ( Poly₁ ‘ 𝐸 ) )
	minplynzm1p.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
	minplynzm1p.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	minplynzm1p.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
	minplynzm1p.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
	minplynzm1p.1	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≠ 𝑍 )
	minplynzm1p.u	⊢ 𝑈 = ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) )
Assertion	minplynzm1p	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		minplynzm1p.b	⊢ 𝐵 = ( Base ‘ 𝐸 )
2		minplynzm1p.z	⊢ 𝑍 = ( 0_g ‘ ( Poly₁ ‘ 𝐸 ) )
3		minplynzm1p.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
4		minplynzm1p.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
5		minplynzm1p.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
6		minplynzm1p.a	⊢ ( 𝜑 → 𝐴 ∈ 𝐵 )
7		minplynzm1p.1	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≠ 𝑍 )
8		minplynzm1p.u	⊢ 𝑈 = ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) )
9		eqid	⊢ ( 𝐸 evalSub₁ 𝐹 ) = ( 𝐸 evalSub₁ 𝐹 )
10		eqid	⊢ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) = ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) )
11		eqid	⊢ ( 0_g ‘ 𝐸 ) = ( 0_g ‘ 𝐸 )
12		eqid	⊢ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } = { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) }
13		eqid	⊢ ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) = ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) )
14		eqid	⊢ ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) = ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) )
15	9 10 1 3 4 6 11 12 13 14 5	minplyval	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) )
16		eqid	⊢ ( 𝐸 ↾_s 𝐹 ) = ( 𝐸 ↾_s 𝐹 )
17	16	sdrgdrng	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → ( 𝐸 ↾_s 𝐹 ) ∈ DivRing )
18	4 17	syl	⊢ ( 𝜑 → ( 𝐸 ↾_s 𝐹 ) ∈ DivRing )
19	3	fldcrngd	⊢ ( 𝜑 → 𝐸 ∈ CRing )
20		sdrgsubrg	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
21	4 20	syl	⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
22	9 10 1 19 21 6 11 12	ply1annidl	⊢ ( 𝜑 → { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ∈ ( LIdeal ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
23	15	sneqd	⊢ ( 𝜑 → { ( 𝑀 ‘ 𝐴 ) } = { ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) } )
24	23	fveq2d	⊢ ( 𝜑 → ( ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ‘ { ( 𝑀 ‘ 𝐴 ) } ) = ( ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ‘ { ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) } ) )
25	9 10 1 3 4 6 11 12 13 14	ply1annig1p	⊢ ( 𝜑 → { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } = ( ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ‘ { ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) } ) )
26	24 25	eqtr4d	⊢ ( 𝜑 → ( ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ‘ { ( 𝑀 ‘ 𝐴 ) } ) = { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } )
27	18	drngringd	⊢ ( 𝜑 → ( 𝐸 ↾_s 𝐹 ) ∈ Ring )
28	10	ply1ring	⊢ ( ( 𝐸 ↾_s 𝐹 ) ∈ Ring → ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ∈ Ring )
29	27 28	syl	⊢ ( 𝜑 → ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ∈ Ring )
30	9 10 1 3 4 6 11 12 13 14 5	minplycl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
31		eqid	⊢ ( Poly₁ ‘ 𝐸 ) = ( Poly₁ ‘ 𝐸 )
32		eqid	⊢ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) = ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) )
33	31 16 10 32 21 2	ressply10g	⊢ ( 𝜑 → 𝑍 = ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
34	7 33	neeqtrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≠ ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) )
35		eqid	⊢ ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) = ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) )
36	32 35 13	pidlnz	⊢ ( ( ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ∈ Ring ∧ ( 𝑀 ‘ 𝐴 ) ∈ ( Base ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ∧ ( 𝑀 ‘ 𝐴 ) ≠ ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ) → ( ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ‘ { ( 𝑀 ‘ 𝐴 ) } ) ≠ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } )
37	29 30 34 36	syl3anc	⊢ ( 𝜑 → ( ( RSpan ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ‘ { ( 𝑀 ‘ 𝐴 ) } ) ≠ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } )
38	26 37	eqnetrrd	⊢ ( 𝜑 → { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ≠ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } )
39		eqid	⊢ ( LIdeal ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) = ( LIdeal ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) )
40		eqid	⊢ ( deg₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) = ( deg₁ ‘ ( 𝐸 ↾_s 𝐹 ) )
41	10 14 35 39 40 8	ig1pval3	⊢ ( ( ( 𝐸 ↾_s 𝐹 ) ∈ DivRing ∧ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ∈ ( LIdeal ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) ∧ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ≠ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } ) → ( ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ∈ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ∧ ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ∈ 𝑈 ∧ ( ( deg₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ) = inf ( ( ( deg₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) “ ( { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ∖ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } ) ) , ℝ , < ) ) )
42	18 22 38 41	syl3anc	⊢ ( 𝜑 → ( ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ∈ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ∧ ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ∈ 𝑈 ∧ ( ( deg₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ) = inf ( ( ( deg₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) “ ( { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ∖ { ( 0_g ‘ ( Poly₁ ‘ ( 𝐸 ↾_s 𝐹 ) ) ) } ) ) , ℝ , < ) ) )
43	42	simp2d	⊢ ( 𝜑 → ( ( idlGen_1p ‘ ( 𝐸 ↾_s 𝐹 ) ) ‘ { 𝑞 ∈ dom ( 𝐸 evalSub₁ 𝐹 ) ∣ ( ( ( 𝐸 evalSub₁ 𝐹 ) ‘ 𝑞 ) ‘ 𝐴 ) = ( 0_g ‘ 𝐸 ) } ) ∈ 𝑈 )
44	15 43	eqeltrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑈 )

Metamath Proof Explorer

Theorem minplynzm1p

Proof