Description: The restriction of the category of non-unital rings to the set of unital ring homomorphisms is a category. (Contributed by AV, 4-Mar-2020) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | rngcrescrhmALTV.u | |- ( ph -> U e. V ) |
|
| rngcrescrhmALTV.c | |- C = ( RngCatALTV ` U ) |
||
| rngcrescrhmALTV.r | |- ( ph -> R = ( Ring i^i U ) ) |
||
| rngcrescrhmALTV.h | |- H = ( RingHom |` ( R X. R ) ) |
||
| Assertion | rhmsubcALTVcat | |- ( ph -> ( ( RngCatALTV ` U ) |`cat H ) e. Cat ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rngcrescrhmALTV.u | |- ( ph -> U e. V ) |
|
| 2 | rngcrescrhmALTV.c | |- C = ( RngCatALTV ` U ) |
|
| 3 | rngcrescrhmALTV.r | |- ( ph -> R = ( Ring i^i U ) ) |
|
| 4 | rngcrescrhmALTV.h | |- H = ( RingHom |` ( R X. R ) ) |
|
| 5 | eqid | |- ( ( RngCatALTV ` U ) |`cat H ) = ( ( RngCatALTV ` U ) |`cat H ) |
|
| 6 | 1 2 3 4 | rhmsubcALTV | |- ( ph -> H e. ( Subcat ` ( RngCatALTV ` U ) ) ) |
| 7 | 5 6 | subccat | |- ( ph -> ( ( RngCatALTV ` U ) |`cat H ) e. Cat ) |