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 = 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 fldhmsubcALTV U V F Subcat RingCatALTV U cat J

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 elin r DivRing CRing r DivRing r CRing
6 5 simprbi r DivRing CRing r CRing
7 crngring r CRing r Ring
8 6 7 syl r DivRing CRing r Ring
9 df-field Field = DivRing CRing
10 8 9 eleq2s r Field r Ring
11 10 rgen r Field r Ring
12 11 3 4 srhmsubcALTV U V F Subcat RingCatALTV U
13 inss1 DivRing CRing DivRing
14 9 13 eqsstri Field DivRing
15 sslin Field DivRing U Field U DivRing
16 14 15 ax-mp U Field U DivRing
17 16 a1i U V U Field U DivRing
18 3 1 sseq12i D C U Field U DivRing
19 17 18 sylibr U V D C
20 ssidd U V x D y D x RingHom y x RingHom y
21 4 a1i U V x D y D F = r D , s D r RingHom s
22 oveq12 r = x s = y r RingHom s = x RingHom y
23 22 adantl U V x D y D r = x s = y r RingHom s = x RingHom y
24 simprl U V x D y D x D
25 simpr x D y D y D
26 25 adantl U V x D y D y D
27 ovexd U V x D y D x RingHom y V
28 21 23 24 26 27 ovmpod U V x D y D x F y = x RingHom y
29 2 a1i U V x D y D J = r C , s C r RingHom s
30 16 18 mpbir D C
31 30 sseli x D x C
32 31 ad2antrl U V x D y D x C
33 30 sseli y D y C
34 33 adantl x D y D y C
35 34 adantl U V x D y D y C
36 29 23 32 35 27 ovmpod U V x D y D x J y = x RingHom y
37 20 28 36 3sstr4d U V x D y D x F y x J y
38 37 ralrimivva U V x D y D x F y x J y
39 ovex r RingHom s V
40 4 39 fnmpoi F Fn D × D
41 40 a1i U V F Fn D × D
42 2 39 fnmpoi J Fn C × C
43 42 a1i U V J Fn C × C
44 inex1g U V U DivRing V
45 1 44 eqeltrid U V C V
46 41 43 45 isssc U V F cat J D C x D y D x F y x J y
47 19 38 46 mpbir2and U V F cat J
48 1 2 drhmsubcALTV U V J Subcat RingCatALTV U
49 eqid RingCatALTV U cat J = RingCatALTV U cat J
50 49 subsubc J Subcat RingCatALTV U F Subcat RingCatALTV U cat J F Subcat RingCatALTV U F cat J
51 48 50 syl U V F Subcat RingCatALTV U cat J F Subcat RingCatALTV U F cat J
52 12 47 51 mpbir2and U V F Subcat RingCatALTV U cat J