# 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}=\mathrm{RingCat}\left({U}\right)$
ringcval.u ${⊢}{\phi }\to {U}\in {V}$
ringcval.b ${⊢}{\phi }\to {B}={U}\cap \mathrm{Ring}$
ringcval.h ${⊢}{\phi }\to {H}={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$
Assertion ringcval ${⊢}{\phi }\to {C}=\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}{H}$

### Proof

Step Hyp Ref Expression
1 ringcval.c ${⊢}{C}=\mathrm{RingCat}\left({U}\right)$
2 ringcval.u ${⊢}{\phi }\to {U}\in {V}$
3 ringcval.b ${⊢}{\phi }\to {B}={U}\cap \mathrm{Ring}$
4 ringcval.h ${⊢}{\phi }\to {H}={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$
5 df-ringc ${⊢}\mathrm{RingCat}=\left({u}\in \mathrm{V}⟼\mathrm{ExtStrCat}\left({u}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left(\left({u}\cap \mathrm{Ring}\right)×\left({u}\cap \mathrm{Ring}\right)\right)}\right)\right)$
6 fveq2 ${⊢}{u}={U}\to \mathrm{ExtStrCat}\left({u}\right)=\mathrm{ExtStrCat}\left({U}\right)$
7 6 adantl ${⊢}\left({\phi }\wedge {u}={U}\right)\to \mathrm{ExtStrCat}\left({u}\right)=\mathrm{ExtStrCat}\left({U}\right)$
8 ineq1 ${⊢}{u}={U}\to {u}\cap \mathrm{Ring}={U}\cap \mathrm{Ring}$
9 8 sqxpeqd ${⊢}{u}={U}\to \left({u}\cap \mathrm{Ring}\right)×\left({u}\cap \mathrm{Ring}\right)=\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)$
10 3 sqxpeqd ${⊢}{\phi }\to {B}×{B}=\left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)$
11 10 eqcomd ${⊢}{\phi }\to \left({U}\cap \mathrm{Ring}\right)×\left({U}\cap \mathrm{Ring}\right)={B}×{B}$
12 9 11 sylan9eqr ${⊢}\left({\phi }\wedge {u}={U}\right)\to \left({u}\cap \mathrm{Ring}\right)×\left({u}\cap \mathrm{Ring}\right)={B}×{B}$
13 12 reseq2d ${⊢}\left({\phi }\wedge {u}={U}\right)\to {\mathrm{RingHom}↾}_{\left(\left({u}\cap \mathrm{Ring}\right)×\left({u}\cap \mathrm{Ring}\right)\right)}={\mathrm{RingHom}↾}_{\left({B}×{B}\right)}$
14 4 eqcomd ${⊢}{\phi }\to {\mathrm{RingHom}↾}_{\left({B}×{B}\right)}={H}$
15 14 adantr ${⊢}\left({\phi }\wedge {u}={U}\right)\to {\mathrm{RingHom}↾}_{\left({B}×{B}\right)}={H}$
16 13 15 eqtrd ${⊢}\left({\phi }\wedge {u}={U}\right)\to {\mathrm{RingHom}↾}_{\left(\left({u}\cap \mathrm{Ring}\right)×\left({u}\cap \mathrm{Ring}\right)\right)}={H}$
17 7 16 oveq12d ${⊢}\left({\phi }\wedge {u}={U}\right)\to \mathrm{ExtStrCat}\left({u}\right){↾}_{\mathrm{cat}}\left({\mathrm{RingHom}↾}_{\left(\left({u}\cap \mathrm{Ring}\right)×\left({u}\cap \mathrm{Ring}\right)\right)}\right)=\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}{H}$
18 2 elexd ${⊢}{\phi }\to {U}\in \mathrm{V}$
19 ovexd ${⊢}{\phi }\to \mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}{H}\in \mathrm{V}$
20 5 17 18 19 fvmptd2 ${⊢}{\phi }\to \mathrm{RingCat}\left({U}\right)=\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}{H}$
21 1 20 syl5eq ${⊢}{\phi }\to {C}=\mathrm{ExtStrCat}\left({U}\right){↾}_{\mathrm{cat}}{H}$