Metamath Proof Explorer


Theorem fldcALTV

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) (New usage is discouraged.)

Ref Expression
Hypotheses drhmsubcALTV.c C = U DivRing
drhmsubcALTV.j J = r C , s C r RingHom s
fldhmsubcALTV.d D = U Field
fldhmsubcALTV.f F = r D , s D r RingHom s
Assertion fldcALTV U V RingCatALTV U cat J cat F Cat

Proof

Step Hyp Ref Expression
1 drhmsubcALTV.c C = U DivRing
2 drhmsubcALTV.j J = r C , s C r RingHom s
3 fldhmsubcALTV.d D = U Field
4 fldhmsubcALTV.f F = r D , s D r RingHom s
5 fvexd U V RingCatALTV U V
6 ovex r RingHom s V
7 2 6 fnmpoi J Fn C × C
8 7 a1i U V J Fn C × C
9 4 6 fnmpoi F Fn D × D
10 9 a1i U V F Fn D × D
11 inex1g U V U DivRing V
12 1 11 eqeltrid U V C V
13 df-field Field = DivRing CRing
14 inss1 DivRing CRing DivRing
15 13 14 eqsstri Field DivRing
16 sslin Field DivRing U Field U DivRing
17 15 16 mp1i U V U Field U DivRing
18 17 3 1 3sstr4g U V D C
19 5 8 10 12 18 rescabs U V RingCatALTV U cat J cat F = RingCatALTV U cat F
20 1 2 3 4 fldcatALTV U V RingCatALTV U cat F Cat
21 19 20 eqeltrd U V RingCatALTV U cat J cat F Cat