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

Metamath Proof Explorer

Theorem fldhmsubc

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)

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

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 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 srhmsubc 
 |-  ( U e. V -> F e. ( Subcat ` ( RingCat ` 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 drhmsubc 
 |-  ( U e. V -> J e. ( Subcat ` ( RingCat ` U ) ) )
49 eqid 
 |-  ( ( RingCat ` U ) |`cat J ) = ( ( RingCat ` U ) |`cat J )
50 49 subsubc 
 |-  ( J e. ( Subcat ` ( RingCat ` U ) ) -> ( F e. ( Subcat ` ( ( RingCat ` U ) |`cat J ) ) <-> ( F e. ( Subcat ` ( RingCat ` U ) ) /\ F C_cat J ) ) )
51 48 50 syl 
 |-  ( U e. V -> ( F e. ( Subcat ` ( ( RingCat ` U ) |`cat J ) ) <-> ( F e. ( Subcat ` ( RingCat ` U ) ) /\ F C_cat J ) ) )
52 12 47 51 mpbir2and 
 |-  ( U e. V -> F e. ( Subcat ` ( ( RingCat ` U ) |`cat J ) ) )