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 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 fldhmsubcALTV
|- ( U e. V -> F e. ( Subcat ` ( ( RingCatALTV ` U ) |`cat J ) ) )

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