Theorem algextdeglem1

Description: Lemma for algextdeg . (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 𝐹 ) )
Assertion	algextdeglem1	⊢ ( 𝜑 → ( 𝐿 ↾s 𝐹 ) = 𝐾 )

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	2	oveq1i	⊢ ( 𝐿 ↾s 𝐹 ) = ( ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ↾s 𝐹 )
9		ovex	⊢ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ V
10		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
11		issdrg	⊢ ( 𝐹 ∈ ( SubDRing ‘ 𝐸 ) ↔ ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
12	6 11	sylib	⊢ ( 𝜑 → ( 𝐸 ∈ DivRing ∧ 𝐹 ∈ ( SubRing ‘ 𝐸 ) ∧ ( 𝐸 ↾s 𝐹 ) ∈ DivRing ) )
13	12	simp1d	⊢ ( 𝜑 → 𝐸 ∈ DivRing )
14	12	simp2d	⊢ ( 𝜑 → 𝐹 ∈ ( SubRing ‘ 𝐸 ) )
15		subrgsubg	⊢ ( 𝐹 ∈ ( SubRing ‘ 𝐸 ) → 𝐹 ∈ ( SubGrp ‘ 𝐸 ) )
16	10	subgss	⊢ ( 𝐹 ∈ ( SubGrp ‘ 𝐸 ) → 𝐹 ⊆ ( Base ‘ 𝐸 ) )
17	14 15 16	3syl	⊢ ( 𝜑 → 𝐹 ⊆ ( Base ‘ 𝐸 ) )
18		eqid	⊢ ( 𝐸 evalSub1 𝐹 ) = ( 𝐸 evalSub1 𝐹 )
19		eqid	⊢ ( 0g ‘ 𝐸 ) = ( 0g ‘ 𝐸 )
20	5	fldcrngd	⊢ ( 𝜑 → 𝐸 ∈ CRing )
21	18 1 10 19 20 14	irngssv	⊢ ( 𝜑 → ( 𝐸 IntgRing 𝐹 ) ⊆ ( Base ‘ 𝐸 ) )
22	21 7	sseldd	⊢ ( 𝜑 → 𝐴 ∈ ( Base ‘ 𝐸 ) )
23	22	snssd	⊢ ( 𝜑 → { 𝐴 } ⊆ ( Base ‘ 𝐸 ) )
24	17 23	unssd	⊢ ( 𝜑 → ( 𝐹 ∪ { 𝐴 } ) ⊆ ( Base ‘ 𝐸 ) )
25	10 13 24	fldgenssid	⊢ ( 𝜑 → ( 𝐹 ∪ { 𝐴 } ) ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
26	25	unssad	⊢ ( 𝜑 → 𝐹 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) )
27		ressabs	⊢ ( ( ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ∈ V ∧ 𝐹 ⊆ ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) → ( ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ↾s 𝐹 ) = ( 𝐸 ↾s 𝐹 ) )
28	9 26 27	sylancr	⊢ ( 𝜑 → ( ( 𝐸 ↾s ( 𝐸 fldGen ( 𝐹 ∪ { 𝐴 } ) ) ) ↾s 𝐹 ) = ( 𝐸 ↾s 𝐹 ) )
29	8 28	eqtrid	⊢ ( 𝜑 → ( 𝐿 ↾s 𝐹 ) = ( 𝐸 ↾s 𝐹 ) )
30	29 1	eqtr4di	⊢ ( 𝜑 → ( 𝐿 ↾s 𝐹 ) = 𝐾 )