Metamath Proof Explorer

Theorem algextdeglem1

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

Ref Expression
Hypotheses algextdeg.k 
|- K = ( E |`s F )
algextdeg.l 
|- L = ( E |`s ( E fldGen ( F u. { A } ) ) )
algextdeg.d 
|- D = ( deg1 ` E )
algextdeg.m 
|- M = ( E minPoly F )
algextdeg.f 
|- ( ph -> E e. Field )
algextdeg.e 
|- ( ph -> F e. ( SubDRing ` E ) )
algextdeg.a 
|- ( ph -> A e. ( E IntgRing F ) )
Assertion algextdeglem1 
|- ( ph -> ( L |`s F ) = K )

Proof

Step Hyp Ref Expression
1 algextdeg.k 
 |-  K = ( E |`s F )
2 algextdeg.l 
 |-  L = ( E |`s ( E fldGen ( F u. { A } ) ) )
3 algextdeg.d 
 |-  D = ( deg1 ` E )
4 algextdeg.m 
 |-  M = ( E minPoly F )
5 algextdeg.f 
 |-  ( ph -> E e. Field )
6 algextdeg.e 
 |-  ( ph -> F e. ( SubDRing ` E ) )
7 algextdeg.a 
 |-  ( ph -> A e. ( E IntgRing F ) )
8 2 oveq1i 
 |-  ( L |`s F ) = ( ( E |`s ( E fldGen ( F u. { A } ) ) ) |`s F )
9 ovex 
 |-  ( E fldGen ( F u. { A } ) ) e. _V
10 eqid 
 |-  ( Base ` E ) = ( Base ` E )
11 issdrg 
 |-  ( F e. ( SubDRing ` E ) <-> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
12 6 11 sylib 
 |-  ( ph -> ( E e. DivRing /\ F e. ( SubRing ` E ) /\ ( E |`s F ) e. DivRing ) )
13 12 simp1d 
 |-  ( ph -> E e. DivRing )
14 12 simp2d 
 |-  ( ph -> F e. ( SubRing ` E ) )
15 subrgsubg 
 |-  ( F e. ( SubRing ` E ) -> F e. ( SubGrp ` E ) )
16 10 subgss 
 |-  ( F e. ( SubGrp ` E ) -> F C_ ( Base ` E ) )
17 14 15 16 3syl 
 |-  ( ph -> F C_ ( Base ` E ) )
18 eqid 
 |-  ( E evalSub1 F ) = ( E evalSub1 F )
19 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
20 5 fldcrngd 
 |-  ( ph -> E e. CRing )
21 18 1 10 19 20 14 irngssv 
 |-  ( ph -> ( E IntgRing F ) C_ ( Base ` E ) )
22 21 7 sseldd 
 |-  ( ph -> A e. ( Base ` E ) )
23 22 snssd 
 |-  ( ph -> { A } C_ ( Base ` E ) )
24 17 23 unssd 
 |-  ( ph -> ( F u. { A } ) C_ ( Base ` E ) )
25 10 13 24 fldgenssid 
 |-  ( ph -> ( F u. { A } ) C_ ( E fldGen ( F u. { A } ) ) )
26 25 unssad 
 |-  ( ph -> F C_ ( E fldGen ( F u. { A } ) ) )
27 ressabs 
 |-  ( ( ( E fldGen ( F u. { A } ) ) e. _V /\ F C_ ( E fldGen ( F u. { A } ) ) ) -> ( ( E |`s ( E fldGen ( F u. { A } ) ) ) |`s F ) = ( E |`s F ) )
28 9 26 27 sylancr 
 |-  ( ph -> ( ( E |`s ( E fldGen ( F u. { A } ) ) ) |`s F ) = ( E |`s F ) )
29 8 28 eqtrid 
 |-  ( ph -> ( L |`s F ) = ( E |`s F ) )
30 29 1 eqtr4di 
 |-  ( ph -> ( L |`s F ) = K )