Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( F e. oField /\ ( F |`s A ) e. Field ) -> ( F |`s A ) e. Field ) |
2 |
|
isofld |
|- ( F e. oField <-> ( F e. Field /\ F e. oRing ) ) |
3 |
2
|
simprbi |
|- ( F e. oField -> F e. oRing ) |
4 |
3
|
adantr |
|- ( ( F e. oField /\ ( F |`s A ) e. Field ) -> F e. oRing ) |
5 |
|
isfld |
|- ( ( F |`s A ) e. Field <-> ( ( F |`s A ) e. DivRing /\ ( F |`s A ) e. CRing ) ) |
6 |
5
|
simprbi |
|- ( ( F |`s A ) e. Field -> ( F |`s A ) e. CRing ) |
7 |
|
crngring |
|- ( ( F |`s A ) e. CRing -> ( F |`s A ) e. Ring ) |
8 |
1 6 7
|
3syl |
|- ( ( F e. oField /\ ( F |`s A ) e. Field ) -> ( F |`s A ) e. Ring ) |
9 |
|
suborng |
|- ( ( F e. oRing /\ ( F |`s A ) e. Ring ) -> ( F |`s A ) e. oRing ) |
10 |
4 8 9
|
syl2anc |
|- ( ( F e. oField /\ ( F |`s A ) e. Field ) -> ( F |`s A ) e. oRing ) |
11 |
|
isofld |
|- ( ( F |`s A ) e. oField <-> ( ( F |`s A ) e. Field /\ ( F |`s A ) e. oRing ) ) |
12 |
1 10 11
|
sylanbrc |
|- ( ( F e. oField /\ ( F |`s A ) e. Field ) -> ( F |`s A ) e. oField ) |