Theorem fldc

Description: The restriction of the category of division rings to the set of field homomorphisms is a category, the "category of fields". (Contributed by AV, 20-Feb-2020)

	Ref	Expression
Hypotheses	drhmsubc.c	$$⊢C=U\cap \mathrm{DivRing}$$
	drhmsubc.j	$$⊢J=\left(r\in C,s\in C⟼r\mathrm{RingHom}s\right)$$
	fldhmsubc.d	$$⊢D=U\cap \mathrm{Field}$$
	fldhmsubc.f	$$⊢F=\left(r\in D,s\in D⟼r\mathrm{RingHom}s\right)$$
Assertion	fldc	$$⊢U\in V\to \left(\mathrm{RingCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}J\right){\upharpoonright }_{\mathrm{cat}}F\in \mathrm{Cat}$$

Proof

Step	Hyp	Ref	Expression
1		drhmsubc.c	$$⊢C=U\cap \mathrm{DivRing}$$
2		drhmsubc.j	$$⊢J=\left(r\in C,s\in C⟼r\mathrm{RingHom}s\right)$$
3		fldhmsubc.d	$$⊢D=U\cap \mathrm{Field}$$
4		fldhmsubc.f	$$⊢F=\left(r\in D,s\in D⟼r\mathrm{RingHom}s\right)$$
5		fvexd	$$⊢U\in V\to \mathrm{RingCat}\left(U\right)\in \mathrm{V}$$
6		ovex	$$⊢r\mathrm{RingHom}s\in \mathrm{V}$$
7	2 6	fnmpoi	$$⊢JFn\left(C\times C\right)$$
8	7	a1i	$$⊢U\in V\to JFn\left(C\times C\right)$$
9	4 6	fnmpoi	$$⊢FFn\left(D\times D\right)$$
10	9	a1i	$$⊢U\in V\to FFn\left(D\times D\right)$$
11		inex1g	$$⊢U\in V\to U\cap \mathrm{DivRing}\in \mathrm{V}$$
12	1 11	eqeltrid	$$⊢U\in V\to C\in \mathrm{V}$$
13		df-field	$$⊢\mathrm{Field}=\mathrm{DivRing}\cap \mathrm{CRing}$$
14		inss1	$$⊢\mathrm{DivRing}\cap \mathrm{CRing}\subseteq \mathrm{DivRing}$$
15	13 14	eqsstri	$$⊢\mathrm{Field}\subseteq \mathrm{DivRing}$$
16		sslin	$$⊢\mathrm{Field}\subseteq \mathrm{DivRing}\to U\cap \mathrm{Field}\subseteq U\cap \mathrm{DivRing}$$
17	15 16	mp1i	$$⊢U\in V\to U\cap \mathrm{Field}\subseteq U\cap \mathrm{DivRing}$$
18	17 3 1	3sstr4g	$$⊢U\in V\to D\subseteq C$$
19	5 8 10 12 18	rescabs	$$⊢U\in V\to \left(\mathrm{RingCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}J\right){\upharpoonright }_{\mathrm{cat}}F=\mathrm{RingCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}F$$
20	1 2 3 4	fldcat	$$⊢U\in V\to \mathrm{RingCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}F\in \mathrm{Cat}$$
21	19 20	eqeltrd	$$⊢U\in V\to \left(\mathrm{RingCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}J\right){\upharpoonright }_{\mathrm{cat}}F\in \mathrm{Cat}$$