Metamath Proof Explorer


Theorem fldhmsubcALTV

Description: According to df-subc , the subcategories ( SubcatC ) of a category C are subsets of the homomorphisms of C (see subcssc and subcss2 ). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020) (New usage is discouraged.)

Ref Expression
Hypotheses drhmsubcALTV.c C=UDivRing
drhmsubcALTV.j J=rC,sCrRingHoms
fldhmsubcALTV.d D=UField
fldhmsubcALTV.f F=rD,sDrRingHoms
Assertion fldhmsubcALTV UVFSubcatRingCatALTVUcatJ

Proof

Step Hyp Ref Expression
1 drhmsubcALTV.c C=UDivRing
2 drhmsubcALTV.j J=rC,sCrRingHoms
3 fldhmsubcALTV.d D=UField
4 fldhmsubcALTV.f F=rD,sDrRingHoms
5 elin rDivRingCRingrDivRingrCRing
6 5 simprbi rDivRingCRingrCRing
7 crngring rCRingrRing
8 6 7 syl rDivRingCRingrRing
9 df-field Field=DivRingCRing
10 8 9 eleq2s rFieldrRing
11 10 rgen rFieldrRing
12 11 3 4 srhmsubcALTV UVFSubcatRingCatALTVU
13 inss1 DivRingCRingDivRing
14 9 13 eqsstri FieldDivRing
15 sslin FieldDivRingUFieldUDivRing
16 14 15 ax-mp UFieldUDivRing
17 16 a1i UVUFieldUDivRing
18 3 1 sseq12i DCUFieldUDivRing
19 17 18 sylibr UVDC
20 ssidd UVxDyDxRingHomyxRingHomy
21 4 a1i UVxDyDF=rD,sDrRingHoms
22 oveq12 r=xs=yrRingHoms=xRingHomy
23 22 adantl UVxDyDr=xs=yrRingHoms=xRingHomy
24 simprl UVxDyDxD
25 simpr xDyDyD
26 25 adantl UVxDyDyD
27 ovexd UVxDyDxRingHomyV
28 21 23 24 26 27 ovmpod UVxDyDxFy=xRingHomy
29 2 a1i UVxDyDJ=rC,sCrRingHoms
30 16 18 mpbir DC
31 30 sseli xDxC
32 31 ad2antrl UVxDyDxC
33 30 sseli yDyC
34 33 adantl xDyDyC
35 34 adantl UVxDyDyC
36 29 23 32 35 27 ovmpod UVxDyDxJy=xRingHomy
37 20 28 36 3sstr4d UVxDyDxFyxJy
38 37 ralrimivva UVxDyDxFyxJy
39 ovex rRingHomsV
40 4 39 fnmpoi FFnD×D
41 40 a1i UVFFnD×D
42 2 39 fnmpoi JFnC×C
43 42 a1i UVJFnC×C
44 inex1g UVUDivRingV
45 1 44 eqeltrid UVCV
46 41 43 45 isssc UVFcatJDCxDyDxFyxJy
47 19 38 46 mpbir2and UVFcatJ
48 1 2 drhmsubcALTV UVJSubcatRingCatALTVU
49 eqid RingCatALTVUcatJ=RingCatALTVUcatJ
50 49 subsubc JSubcatRingCatALTVUFSubcatRingCatALTVUcatJFSubcatRingCatALTVUFcatJ
51 48 50 syl UVFSubcatRingCatALTVUcatJFSubcatRingCatALTVUFcatJ
52 12 47 51 mpbir2and UVFSubcatRingCatALTVUcatJ