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 ) ) )