This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fldc

Description: The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020)

Ref Expression
Hypotheses drhmsubc.c 
|- C = ( U i^i DivRing )
drhmsubc.j 
|- J = ( r e. C , s e. C |-> ( r RingHom s ) )
fldhmsubc.d 
|- D = ( U i^i Field )
fldhmsubc.f 
|- F = ( r e. D , s e. D |-> ( r RingHom s ) )
Assertion fldc 
|- ( U e. V -> ( ( ( RingCat ` U ) |`cat J ) |`cat F ) e. Cat )

Proof

Step Hyp Ref Expression
1 drhmsubc.c 
 |-  C = ( U i^i DivRing )
2 drhmsubc.j 
 |-  J = ( r e. C , s e. C |-> ( r RingHom s ) )
3 fldhmsubc.d 
 |-  D = ( U i^i Field )
4 fldhmsubc.f 
 |-  F = ( r e. D , s e. D |-> ( r RingHom s ) )
5 fvexd 
 |-  ( U e. V -> ( RingCat ` U ) e. _V )
6 ovex 
 |-  ( r RingHom s ) e. _V
7 2 6 fnmpoi 
 |-  J Fn ( C X. C )
8 7 a1i 
 |-  ( U e. V -> J Fn ( C X. C ) )
9 4 6 fnmpoi 
 |-  F Fn ( D X. D )
10 9 a1i 
 |-  ( U e. V -> F Fn ( D X. D ) )
11 inex1g 
 |-  ( U e. V -> ( U i^i DivRing ) e. _V )
12 1 11 eqeltrid 
 |-  ( U e. V -> C e. _V )
13 df-field 
 |-  Field = ( DivRing i^i CRing )
14 inss1 
 |-  ( DivRing i^i CRing ) C_ DivRing
15 13 14 eqsstri 
 |-  Field C_ DivRing
16 sslin 
 |-  ( Field C_ DivRing -> ( U i^i Field ) C_ ( U i^i DivRing ) )
17 15 16 mp1i 
 |-  ( U e. V -> ( U i^i Field ) C_ ( U i^i DivRing ) )
18 17 3 1 3sstr4g 
 |-  ( U e. V -> D C_ C )
19 5 8 10 12 18 rescabs 
 |-  ( U e. V -> ( ( ( RingCat ` U ) |`cat J ) |`cat F ) = ( ( RingCat ` U ) |`cat F ) )
20 1 2 3 4 fldcat 
 |-  ( U e. V -> ( ( RingCat ` U ) |`cat F ) e. Cat )
21 19 20 eqeltrd 
 |-  ( U e. V -> ( ( ( RingCat ` U ) |`cat J ) |`cat F ) e. Cat )