Metamath Proof Explorer


Theorem fldcatALTV

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 )

Proof

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 )