minplym1p

Description: A minimal polynomial is monic. (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	irngnminplynz.z	⊢ 𝑍 = ( 0_g ‘ ( Poly₁ ‘ 𝐸 ) )
	irngnminplynz.e	⊢ ( 𝜑 → 𝐸 ∈ Field )
	irngnminplynz.f	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	irngnminplynz.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
	irngnminplynz.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
	minplym1p.1	⊢ 𝑈 = ( Monic_1p ‘ ( 𝐸 ↾_s 𝐹 ) )
Assertion	minplym1p	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ 𝑈 )

Proof

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

Metamath Proof Explorer

Theorem minplym1p

Proof