| Step |
Hyp |
Ref |
Expression |
| 1 |
|
orng0le1.1 |
|- .0. = ( 0g ` F ) |
| 2 |
|
orng0le1.2 |
|- .1. = ( 1r ` F ) |
| 3 |
|
ofld0lt1.3 |
|- .< = ( lt ` F ) |
| 4 |
|
isofld |
|- ( F e. oField <-> ( F e. Field /\ F e. oRing ) ) |
| 5 |
4
|
simprbi |
|- ( F e. oField -> F e. oRing ) |
| 6 |
|
eqid |
|- ( le ` F ) = ( le ` F ) |
| 7 |
1 2 6
|
orng0le1 |
|- ( F e. oRing -> .0. ( le ` F ) .1. ) |
| 8 |
5 7
|
syl |
|- ( F e. oField -> .0. ( le ` F ) .1. ) |
| 9 |
|
ofldfld |
|- ( F e. oField -> F e. Field ) |
| 10 |
|
isfld |
|- ( F e. Field <-> ( F e. DivRing /\ F e. CRing ) ) |
| 11 |
10
|
simplbi |
|- ( F e. Field -> F e. DivRing ) |
| 12 |
1 2
|
drngunz |
|- ( F e. DivRing -> .1. =/= .0. ) |
| 13 |
9 11 12
|
3syl |
|- ( F e. oField -> .1. =/= .0. ) |
| 14 |
13
|
necomd |
|- ( F e. oField -> .0. =/= .1. ) |
| 15 |
1
|
fvexi |
|- .0. e. _V |
| 16 |
2
|
fvexi |
|- .1. e. _V |
| 17 |
6 3
|
pltval |
|- ( ( F e. oField /\ .0. e. _V /\ .1. e. _V ) -> ( .0. .< .1. <-> ( .0. ( le ` F ) .1. /\ .0. =/= .1. ) ) ) |
| 18 |
15 16 17
|
mp3an23 |
|- ( F e. oField -> ( .0. .< .1. <-> ( .0. ( le ` F ) .1. /\ .0. =/= .1. ) ) ) |
| 19 |
8 14 18
|
mpbir2and |
|- ( F e. oField -> .0. .< .1. ) |