Metamath Proof Explorer


Theorem ringcval

Description: Value of the category of unital rings (in a universe). (Contributed by AV, 13-Feb-2020) (Revised by AV, 8-Mar-2020)

Ref Expression
Hypotheses ringcval.c C = RingCat U
ringcval.u φ U V
ringcval.b φ B = U Ring
ringcval.h φ H = RingHom B × B
Assertion ringcval φ C = ExtStrCat U cat H

Proof

Step Hyp Ref Expression
1 ringcval.c C = RingCat U
2 ringcval.u φ U V
3 ringcval.b φ B = U Ring
4 ringcval.h φ H = RingHom B × B
5 df-ringc RingCat = u V ExtStrCat u cat RingHom u Ring × u Ring
6 fveq2 u = U ExtStrCat u = ExtStrCat U
7 6 adantl φ u = U ExtStrCat u = ExtStrCat U
8 ineq1 u = U u Ring = U Ring
9 8 sqxpeqd u = U u Ring × u Ring = U Ring × U Ring
10 3 sqxpeqd φ B × B = U Ring × U Ring
11 10 eqcomd φ U Ring × U Ring = B × B
12 9 11 sylan9eqr φ u = U u Ring × u Ring = B × B
13 12 reseq2d φ u = U RingHom u Ring × u Ring = RingHom B × B
14 4 eqcomd φ RingHom B × B = H
15 14 adantr φ u = U RingHom B × B = H
16 13 15 eqtrd φ u = U RingHom u Ring × u Ring = H
17 7 16 oveq12d φ u = U ExtStrCat u cat RingHom u Ring × u Ring = ExtStrCat U cat H
18 2 elexd φ U V
19 ovexd φ ExtStrCat U cat H V
20 5 17 18 19 fvmptd2 φ RingCat U = ExtStrCat U cat H
21 1 20 syl5eq φ C = ExtStrCat U cat H