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	⊢ 𝐶 = ( 𝑈 ∩ DivRing )
	drhmsubc.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
	fldhmsubc.d	⊢ 𝐷 = ( 𝑈 ∩ Field )
	fldhmsubc.f	⊢ 𝐹 = ( 𝑟 ∈ 𝐷 , 𝑠 ∈ 𝐷 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion	fldc	⊢ ( 𝑈 ∈ 𝑉 → ( ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) ↾cat 𝐹 ) ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		drhmsubc.c	⊢ 𝐶 = ( 𝑈 ∩ DivRing )
2		drhmsubc.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
3		fldhmsubc.d	⊢ 𝐷 = ( 𝑈 ∩ Field )
4		fldhmsubc.f	⊢ 𝐹 = ( 𝑟 ∈ 𝐷 , 𝑠 ∈ 𝐷 ↦ ( 𝑟 RingHom 𝑠 ) )
5		fvexd	⊢ ( 𝑈 ∈ 𝑉 → ( RingCat ‘ 𝑈 ) ∈ V )
6		ovex	⊢ ( 𝑟 RingHom 𝑠 ) ∈ V
7	2 6	fnmpoi	⊢ 𝐽 Fn ( 𝐶 × 𝐶 )
8	7	a1i	⊢ ( 𝑈 ∈ 𝑉 → 𝐽 Fn ( 𝐶 × 𝐶 ) )
9	4 6	fnmpoi	⊢ 𝐹 Fn ( 𝐷 × 𝐷 )
10	9	a1i	⊢ ( 𝑈 ∈ 𝑉 → 𝐹 Fn ( 𝐷 × 𝐷 ) )
11		inex1g	⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ DivRing ) ∈ V )
12	1 11	eqeltrid	⊢ ( 𝑈 ∈ 𝑉 → 𝐶 ∈ V )
13		df-field	⊢ Field = ( DivRing ∩ CRing )
14		inss1	⊢ ( DivRing ∩ CRing ) ⊆ DivRing
15	13 14	eqsstri	⊢ Field ⊆ DivRing
16		sslin	⊢ ( Field ⊆ DivRing → ( 𝑈 ∩ Field ) ⊆ ( 𝑈 ∩ DivRing ) )
17	15 16	mp1i	⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∩ Field ) ⊆ ( 𝑈 ∩ DivRing ) )
18	17 3 1	3sstr4g	⊢ ( 𝑈 ∈ 𝑉 → 𝐷 ⊆ 𝐶 )
19	5 8 10 12 18	rescabs	⊢ ( 𝑈 ∈ 𝑉 → ( ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) ↾cat 𝐹 ) = ( ( RingCat ‘ 𝑈 ) ↾cat 𝐹 ) )
20	1 2 3 4	fldcat	⊢ ( 𝑈 ∈ 𝑉 → ( ( RingCat ‘ 𝑈 ) ↾cat 𝐹 ) ∈ Cat )
21	19 20	eqeltrd	⊢ ( 𝑈 ∈ 𝑉 → ( ( ( RingCat ‘ 𝑈 ) ↾cat 𝐽 ) ↾cat 𝐹 ) ∈ Cat )