Metamath Proof Explorer

Table of Contents - 21.50.18.6. The category of (unital) rings (alternate definition)

As an alternative to df-ringc, the "category of unital rings" can be defined as extensible structure consisting of three components/slots for the objects, morphisms and composition, according to dfringc2.

1. cringcALTV
2. df-ringcALTV
3. ringcvalALTV
4. funcringcsetcALTV2lem1
5. funcringcsetcALTV2lem2
6. funcringcsetcALTV2lem3
7. funcringcsetcALTV2lem4
8. funcringcsetcALTV2lem5
9. funcringcsetcALTV2lem6
10. funcringcsetcALTV2lem7
11. funcringcsetcALTV2lem8
12. funcringcsetcALTV2lem9
13. funcringcsetcALTV2
14. ringcbasALTV
15. ringchomfvalALTV
16. ringchomALTV
17. elringchomALTV
18. ringccofvalALTV
19. ringccoALTV
20. ringccatidALTV
21. ringccatALTV
22. ringcidALTV
23. ringcsectALTV
24. ringcinvALTV
25. ringcisoALTV
26. ringcbasbasALTV
27. funcringcsetclem1ALTV
28. funcringcsetclem2ALTV
29. funcringcsetclem3ALTV
30. funcringcsetclem4ALTV
31. funcringcsetclem5ALTV
32. funcringcsetclem6ALTV
33. funcringcsetclem7ALTV
34. funcringcsetclem8ALTV
35. funcringcsetclem9ALTV
36. funcringcsetcALTV
37. srhmsubcALTVlem1
38. srhmsubcALTVlem2
39. srhmsubcALTV
40. sringcatALTV
41. crhmsubcALTV
42. cringcatALTV
43. drhmsubcALTV
44. drngcatALTV
45. fldcatALTV
46. fldcALTV
47. fldhmsubcALTV