| 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 ) |