This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐹 ) = 𝐾 )