Theorem algextdeglem5

Description: Lemma for algextdeg . The subspace Z of annihilators of A is a principal ideal generated by the minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025)

	Ref	Expression
Hypotheses	algextdeg.k	⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
	algextdeg.l	⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
	algextdeg.d	⊢ 𝐷 = ( deg1 ‘ 𝐸 )
	algextdeg.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
	algextdeg.f	⊢ ( 𝜑 → 𝐸 ∈ Field )
	algextdeg.e	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
	algextdeg.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
	algextdeglem.o	⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
	algextdeglem.y	⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
	algextdeglem.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	algextdeglem.g	⊢ 𝐺 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
	algextdeglem.n	⊢ 𝑁 = ( 𝑥 ∈ 𝑈 ↦ [ 𝑥 ] ( 𝑃 ~QG 𝑍 ) )
	algextdeglem.z	⊢ 𝑍 = ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } )
	algextdeglem.q	⊢ 𝑄 = ( 𝑃 /s ( 𝑃 ~QG 𝑍 ) )
	algextdeglem.j	⊢ 𝐽 = ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐺 “ 𝑝 ) )
Assertion	algextdeglem5	⊢ ( 𝜑 → 𝑍 = ( ( RSpan ‘ 𝑃 ) ‘ { ( 𝑀 ‘ 𝐴 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		algextdeg.k	⊢ 𝐾 = ( 𝐸 ↾s 𝐹 )
2		algextdeg.l	⊢ 𝐿 = ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
3		algextdeg.d	⊢ 𝐷 = ( deg1 ‘ 𝐸 )
4		algextdeg.m	⊢ 𝑀 = ( 𝐸 minPoly 𝐹 )
5		algextdeg.f	⊢ ( 𝜑 → 𝐸 ∈ Field )
6		algextdeg.e	⊢ ( 𝜑 → 𝐹 ∈ ( SubDRing ‘ 𝐸 ) )
7		algextdeg.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐸 IntgRing 𝐹 ) )
8		algextdeglem.o	⊢ 𝑂 = ( 𝐸 evalSub1 𝐹 )
9		algextdeglem.y	⊢ 𝑃 = ( Poly1 ‘ 𝐾 )
10		algextdeglem.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
11		algextdeglem.g	⊢ 𝐺 = ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
12		algextdeglem.n	⊢ 𝑁 = ( 𝑥 ∈ 𝑈 ↦ [ 𝑥 ] ( 𝑃 ~QG 𝑍 ) )
13		algextdeglem.z	⊢ 𝑍 = ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } )
14		algextdeglem.q	⊢ 𝑄 = ( 𝑃 /s ( 𝑃 ~QG 𝑍 ) )
15		algextdeglem.j	⊢ 𝐽 = ( 𝑝 ∈ ( Base ‘ 𝑄 ) ↦ ∪ ( 𝐺 “ 𝑝 ) )
16	1	fveq2i	⊢ ( Poly1 ‘ 𝐾 ) = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
17	9 16	eqtri	⊢ 𝑃 = ( Poly1 ‘ ( 𝐸 ↾s 𝐹 ) )
18		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
19		eqid	⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
20	5	fldcrngd	⊢ ( 𝜑 → 𝐸 ∈ CRing )
21		issdrg	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
22	6 21	sylib	⊢ ( 𝜑 → ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
23	22	simp2d	⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
24	8 1 18 19 20 23	irngssv	⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
25	24 7	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐸 ) )
26		eqid	⊢ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) }
27		eqid	⊢ ( RSpan ‘ 𝑃 ) = ( RSpan ‘ 𝑃 )
28		eqid	⊢ ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) = ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) )
29	8 17 18 5 6 25 19 26 27 28	ply1annig1p	⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } = ( ( RSpan ‘ 𝑃 ) ‘ { ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ) } ) )
30	20	crnggrpd	⊢ ( 𝜑 → 𝐸 ∈ Grp )
31	30	grpmndd	⊢ ( 𝜑 → 𝐸 ∈ Mnd )
32	5	flddrngd	⊢ ( 𝜑 → 𝐸 ∈ DivRing )
33		subrgsubg	⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → 𝐹 ∈ ( SubGrp ‘ 𝐸 ) )
34	18	subgss	⊢ ( 𝐹 ∈ ( SubGrp ‘ 𝐸 ) → 𝐹 ⊆ ( Base ‘ 𝐸 ) )
35	23 33 34	3syl	⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐸 ) )
36	25	snssd	⊢ ( 𝜑 → { 𝐴 } ⊆ ( Base ‘ 𝐸 ) )
37	35 36	unssd	⊢ ( 𝜑 → ( 𝐹 ∪ { 𝐴 } ) ⊆ ( Base ‘ 𝐸 ) )
38	18 32 37	fldgensdrg	⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ 𝐸 ) )
39		sdrgsubrg	⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubDRing ‘ 𝐸 ) → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) )
40		subrgsubg	⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubRing ‘ 𝐸 ) → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubGrp ‘ 𝐸 ) )
41	19	subg0cl	⊢ ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ ( SubGrp ‘ 𝐸 ) → ( 0g ‘ 𝐸 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
42	38 39 40 41	4syl	⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
43	18 32 37	fldgenssv	⊢ ( 𝜑 → ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ⊆ ( Base ‘ 𝐸 ) )
44	2 18 19	ress0g	⊢ ( ( 𝐸 ∈ Mnd ∧ ( 0g ‘ 𝐸 ) ∈ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∧ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ⊆ ( Base ‘ 𝐸 ) ) → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐿 ) )
45	31 42 43 44	syl3anc	⊢ ( 𝜑 → ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐿 ) )
46	45	sneqd	⊢ ( 𝜑 → { ( 0g ‘ 𝐸 ) } = { ( 0g ‘ 𝐿 ) } )
47	46	imaeq2d	⊢ ( 𝜑 → ( ◡ 𝐺 “ { ( 0g ‘ 𝐸 ) } ) = ( ◡ 𝐺 “ { ( 0g ‘ 𝐿 ) } ) )
48	13 47	eqtr4id	⊢ ( 𝜑 → 𝑍 = ( ◡ 𝐺 “ { ( 0g ‘ 𝐸 ) } ) )
49	10	mpteq1i	⊢ ( 𝑝 ∈ 𝑈 ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) ) = ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
50	11 49	eqtri	⊢ 𝐺 = ( 𝑝 ∈ ( Base ‘ 𝑃 ) ↦ ( ( 𝑂 ‘ 𝑝 ) ‘ 𝐴 ) )
51	8 17 18 20 23 25 19 26 50	ply1annidllem	⊢ ( 𝜑 → { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } = ( ◡ 𝐺 “ { ( 0g ‘ 𝐸 ) } ) )
52	48 51	eqtr4d	⊢ ( 𝜑 → 𝑍 = { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } )
53	8 17 18 5 6 25 19 26 27 28 4	minplyval	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) = ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ) )
54	53	sneqd	⊢ ( 𝜑 → { ( 𝑀 ‘ 𝐴 ) } = { ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ) } )
55	54	fveq2d	⊢ ( 𝜑 → ( ( RSpan ‘ 𝑃 ) ‘ { ( 𝑀 ‘ 𝐴 ) } ) = ( ( RSpan ‘ 𝑃 ) ‘ { ( ( idlGen1p ‘ ( 𝐸 ↾s 𝐹 ) ) ‘ { 𝑞 ∈ dom 𝑂 ∣ ( ( 𝑂 ‘ 𝑞 ) ‘ 𝐴 ) = ( 0g ‘ 𝐸 ) } ) } ) )
56	29 52 55	3eqtr4d	⊢ ( 𝜑 → 𝑍 = ( ( RSpan ‘ 𝑃 ) ‘ { ( 𝑀 ‘ 𝐴 ) } ) )