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

Metamath Proof Explorer

Theorem drngcat

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

	Ref	Expression
Hypotheses	drhmsubc.c	⊢ 𝐶 = ( 𝑈 ∩ DivRing )
	drhmsubc.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion	drngcat	⊢ ( 𝑈 ∈ 𝑉 → ( ( RingCat ‘ 𝑈 ) ↾_cat 𝐽 ) ∈ Cat )

Proof

Step	Hyp	Ref	Expression
1		drhmsubc.c	⊢ 𝐶 = ( 𝑈 ∩ DivRing )
2		drhmsubc.j	⊢ 𝐽 = ( 𝑟 ∈ 𝐶 , 𝑠 ∈ 𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
3		drngring	⊢ ( 𝑟 ∈ DivRing → 𝑟 ∈ Ring )
4	3	rgen	⊢ ∀ 𝑟 ∈ DivRing 𝑟 ∈ Ring
5	4 1 2	sringcat	⊢ ( 𝑈 ∈ 𝑉 → ( ( RingCat ‘ 𝑈 ) ↾_cat 𝐽 ) ∈ Cat )