Theorem fldcat

Description: The restriction of the category of (unital) 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	fldcat	⊢ ( 𝑈 ∈ 𝑉 → ( ( RingCat ‘ 𝑈 ) ↾cat 𝐹 ) ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		drhmsubc.c	⊢ 𝐶 = ( 𝑈 ∩ DivRing )
2		drhmsubc.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
3		fldhmsubc.d	⊢ 𝐷 = ( 𝑈 ∩ Field )
4		fldhmsubc.f	⊢ 𝐹 = ( 𝑟 ∈ 𝐷 , 𝑠 ∈ 𝐷 ↦ ( 𝑟 RingHom 𝑠 ) )
5		isfld	⊢ ( 𝑟 ∈ Field ↔ ( 𝑟 ∈ DivRing ∧ 𝑟 ∈ CRing ) )
6		crngring	⊢ ( 𝑟 ∈ CRing → 𝑟 ∈ Ring )
7	6	adantl	⊢ ( ( 𝑟 ∈ DivRing ∧ 𝑟 ∈ CRing ) → 𝑟 ∈ Ring )
8	5 7	sylbi	⊢ ( 𝑟 ∈ Field → 𝑟 ∈ Ring )
9	8	rgen	⊢ ∀ 𝑟 ∈ Field 𝑟 ∈ Ring
10	9 3 4	sringcat	⊢ ( 𝑈 ∈ 𝑉 → ( ( RingCat ‘ 𝑈 ) ↾cat 𝐹 ) ∈ Cat )