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	|- ( ph -> U e. V )
	ringcval.b	|- ( ph -> B = ( U i^i Ring ) )
	ringcval.h	|- ( ph -> H = ( RingHom |` ( B X. B ) ) )
Assertion	ringcval	|- ( ph -> C = ( ( ExtStrCat ` U ) |`cat H ) )

Proof

Step	Hyp	Ref	Expression
1		ringcval.c	|- C = ( RingCat ` U )
2		ringcval.u	|- ( ph -> U e. V )
3		ringcval.b	|- ( ph -> B = ( U i^i Ring ) )
4		ringcval.h	|- ( ph -> H = ( RingHom |` ( B X. B ) ) )
5		df-ringc	|- RingCat = ( u e. _V |-> ( ( ExtStrCat ` u ) |`cat ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) ) )
6		fveq2	|- ( u = U -> ( ExtStrCat ` u ) = ( ExtStrCat ` U ) )
7	6	adantl	|- ( ( ph /\ u = U ) -> ( ExtStrCat ` u ) = ( ExtStrCat ` U ) )
8		ineq1	|- ( u = U -> ( u i^i Ring ) = ( U i^i Ring ) )
9	8	sqxpeqd	|- ( u = U -> ( ( u i^i Ring ) X. ( u i^i Ring ) ) = ( ( U i^i Ring ) X. ( U i^i Ring ) ) )
10	3	sqxpeqd	|- ( ph -> ( B X. B ) = ( ( U i^i Ring ) X. ( U i^i Ring ) ) )
11	10	eqcomd	|- ( ph -> ( ( U i^i Ring ) X. ( U i^i Ring ) ) = ( B X. B ) )
12	9 11	sylan9eqr	|- ( ( ph /\ u = U ) -> ( ( u i^i Ring ) X. ( u i^i Ring ) ) = ( B X. B ) )
13	12	reseq2d	|- ( ( ph /\ u = U ) -> ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) = ( RingHom |` ( B X. B ) ) )
14	4	eqcomd	|- ( ph -> ( RingHom |` ( B X. B ) ) = H )
15	14	adantr	|- ( ( ph /\ u = U ) -> ( RingHom |` ( B X. B ) ) = H )
16	13 15	eqtrd	|- ( ( ph /\ u = U ) -> ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) = H )
17	7 16	oveq12d	|- ( ( ph /\ u = U ) -> ( ( ExtStrCat ` u ) |`cat ( RingHom |` ( ( u i^i Ring ) X. ( u i^i Ring ) ) ) ) = ( ( ExtStrCat ` U ) |`cat H ) )
18	2	elexd	|- ( ph -> U e. _V )
19		ovexd	|- ( ph -> ( ( ExtStrCat ` U ) |`cat H ) e. _V )
20	5 17 18 19	fvmptd2	|- ( ph -> ( RingCat ` U ) = ( ( ExtStrCat ` U ) |`cat H ) )
21	1 20	eqtrid	|- ( ph -> C = ( ( ExtStrCat ` U ) |`cat H ) )