Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Rings (extension)
Subcategories of the category of rings
drngcatALTV
Metamath Proof Explorer
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 )