Metamath Proof Explorer

Theorem algextdeglem1

Description: Lemma for algextdeg . (Contributed by Thierry Arnoux, 2-Apr-2025)

Ref Expression
Hypotheses algextdeg.k ⊢ K = E ↾ 𝑠 F
algextdeg.l ⊢ L = E ↾ 𝑠 E fldGen F ∪ A
algextdeg.d ⊢ D = deg 1 ⁡ E
algextdeg.m ⊢ M = E minPoly F
algextdeg.f ⊢ φ → E ∈ Field
algextdeg.e ⊢ φ → F ∈ SubDRing ⁡ E
algextdeg.a ⊢ φ → A ∈ E IntgRing F
Assertion algextdeglem1 ⊢ φ → L ↾ 𝑠 F = K

Proof

Step Hyp Ref Expression
1 algextdeg.k ⊢ K = E ↾ 𝑠 F
2 algextdeg.l ⊢ L = E ↾ 𝑠 E fldGen F ∪ A
3 algextdeg.d ⊢ D = deg 1 ⁡ E
4 algextdeg.m ⊢ M = E minPoly F
5 algextdeg.f ⊢ φ → E ∈ Field
6 algextdeg.e ⊢ φ → F ∈ SubDRing ⁡ E
7 algextdeg.a ⊢ φ → A ∈ E IntgRing F
8 2 oveq1i ⊢ L ↾ 𝑠 F = E ↾ 𝑠 E fldGen F ∪ A ↾ 𝑠 F
9 ovex ⊢ E fldGen F ∪ A ∈ V
10 eqid ⊢ Base E = Base E
11 issdrg ⊢ F ∈ SubDRing ⁡ E ↔ E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
12 6 11 sylib ⊢ φ → E ∈ DivRing ∧ F ∈ SubRing ⁡ E ∧ E ↾ 𝑠 F ∈ DivRing
13 12 simp1d ⊢ φ → E ∈ DivRing
14 12 simp2d ⊢ φ → F ∈ SubRing ⁡ E
15 subrgsubg ⊢ F ∈ SubRing ⁡ E → F ∈ SubGrp ⁡ E
16 10 subgss ⊢ F ∈ SubGrp ⁡ E → F ⊆ Base E
17 14 15 16 3syl ⊢ φ → F ⊆ Base E
18 eqid ⊢ E evalSub 1 F = E evalSub 1 F
19 eqid ⊢ 0 E = 0 E
20 5 fldcrngd ⊢ φ → E ∈ CRing
21 18 1 10 19 20 14 irngssv ⊢ φ → E IntgRing F ⊆ Base E
22 21 7 sseldd ⊢ φ → A ∈ Base E
23 22 snssd ⊢ φ → A ⊆ Base E
24 17 23 unssd ⊢ φ → F ∪ A ⊆ Base E
25 10 13 24 fldgenssid ⊢ φ → F ∪ A ⊆ E fldGen F ∪ A
26 25 unssad ⊢ φ → F ⊆ E fldGen F ∪ A
27 ressabs ⊢ E fldGen F ∪ A ∈ V ∧ F ⊆ E fldGen F ∪ A → E ↾ 𝑠 E fldGen F ∪ A ↾ 𝑠 F = E ↾ 𝑠 F
28 9 26 27 sylancr ⊢ φ → E ↾ 𝑠 E fldGen F ∪ A ↾ 𝑠 F = E ↾ 𝑠 F
29 8 28 eqtrid ⊢ φ → L ↾ 𝑠 F = E ↾ 𝑠 F
30 29 1 eqtr4di ⊢ φ → L ↾ 𝑠 F = K