Description: The restriction of the category of (unital) rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | drhmsubcALTV.c | |- C = ( U i^i DivRing ) |
|
| drhmsubcALTV.j | |- J = ( r e. C , s e. C |-> ( r RingHom s ) ) |
||
| fldhmsubcALTV.d | |- D = ( U i^i Field ) |
||
| fldhmsubcALTV.f | |- F = ( r e. D , s e. D |-> ( r RingHom s ) ) |
||
| Assertion | fldcatALTV | |- ( U e. V -> ( ( RingCatALTV ` U ) |`cat F ) e. Cat ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | drhmsubcALTV.c | |- C = ( U i^i DivRing ) |
|
| 2 | drhmsubcALTV.j | |- J = ( r e. C , s e. C |-> ( r RingHom s ) ) |
|
| 3 | fldhmsubcALTV.d | |- D = ( U i^i Field ) |
|
| 4 | fldhmsubcALTV.f | |- F = ( r e. D , s e. D |-> ( r RingHom s ) ) |
|
| 5 | isfld | |- ( r e. Field <-> ( r e. DivRing /\ r e. CRing ) ) |
|
| 6 | crngring | |- ( r e. CRing -> r e. Ring ) |
|
| 7 | 6 | adantl | |- ( ( r e. DivRing /\ r e. CRing ) -> r e. Ring ) |
| 8 | 5 7 | sylbi | |- ( r e. Field -> r e. Ring ) |
| 9 | 8 | rgen | |- A. r e. Field r e. Ring |
| 10 | 9 3 4 | sringcatALTV | |- ( U e. V -> ( ( RingCatALTV ` U ) |`cat F ) e. Cat ) |