Metamath Proof Explorer


Theorem drngcatALTV

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) (New usage is discouraged.)

Ref Expression
Hypotheses drhmsubcALTV.c 𝐶 = ( 𝑈 ∩ DivRing )
drhmsubcALTV.j 𝐽 = ( 𝑟𝐶 , 𝑠𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
Assertion drngcatALTV ( 𝑈𝑉 → ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) ∈ Cat )

Proof

Step Hyp Ref Expression
1 drhmsubcALTV.c 𝐶 = ( 𝑈 ∩ DivRing )
2 drhmsubcALTV.j 𝐽 = ( 𝑟𝐶 , 𝑠𝐶 ↦ ( 𝑟 RingHom 𝑠 ) )
3 drngring ( 𝑟 ∈ DivRing → 𝑟 ∈ Ring )
4 3 rgen 𝑟 ∈ DivRing 𝑟 ∈ Ring
5 4 1 2 sringcatALTV ( 𝑈𝑉 → ( ( RingCatALTV ‘ 𝑈 ) ↾cat 𝐽 ) ∈ Cat )