Description: Obsolete version of fldidom as of 11-Nov-2024. (Contributed by Mario Carneiro, 29-Mar-2015) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | fldidomOLD | |- ( R e. Field -> R e. IDomn ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | isfld | |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) ) |
|
| 2 | 1 | simprbi | |- ( R e. Field -> R e. CRing ) |
| 3 | 1 | simplbi | |- ( R e. Field -> R e. DivRing ) |
| 4 | drngdomn | |- ( R e. DivRing -> R e. Domn ) |
|
| 5 | 3 4 | syl | |- ( R e. Field -> R e. Domn ) |
| 6 | isidom | |- ( R e. IDomn <-> ( R e. CRing /\ R e. Domn ) ) |
|
| 7 | 2 5 6 | sylanbrc | |- ( R e. Field -> R e. IDomn ) |