Step |
Hyp |
Ref |
Expression |
1 |
|
fldextsubrg.1 |
|- U = ( Base ` F ) |
2 |
|
fldextfld1 |
|- ( E /FldExt F -> E e. Field ) |
3 |
|
fldextfld2 |
|- ( E /FldExt F -> F e. Field ) |
4 |
|
brfldext |
|- ( ( E e. Field /\ F e. Field ) -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) ) |
5 |
2 3 4
|
syl2anc |
|- ( E /FldExt F -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) ) |
6 |
5
|
ibi |
|- ( E /FldExt F -> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) |
7 |
6
|
simprd |
|- ( E /FldExt F -> ( Base ` F ) e. ( SubRing ` E ) ) |
8 |
1 7
|
eqeltrid |
|- ( E /FldExt F -> U e. ( SubRing ` E ) ) |