Theorem rngcval

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

	Ref	Expression
Hypotheses	rngcval.c	|- C = ( RngCat ` U )
	rngcval.u	|- ( ph -> U e. V )
	rngcval.b	|- ( ph -> B = ( U i^i Rng ) )
	rngcval.h	|- ( ph -> H = ( RngHom |` ( B X. B ) ) )
Assertion	rngcval	|- ( ph -> C = ( ( ExtStrCat ` U ) |`cat H ) )

Proof

Step	Hyp	Ref	Expression
1		rngcval.c	|- C = ( RngCat ` U )
2		rngcval.u	|- ( ph -> U e. V )
3		rngcval.b	|- ( ph -> B = ( U i^i Rng ) )
4		rngcval.h	|- ( ph -> H = ( RngHom |` ( B X. B ) ) )
5		df-rngc	|- RngCat = ( u e. _V |-> ( ( ExtStrCat ` u ) |`cat ( RngHom |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) ) )
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 Rng ) = ( U i^i Rng ) )
9	8	sqxpeqd	|- ( u = U -> ( ( u i^i Rng ) X. ( u i^i Rng ) ) = ( ( U i^i Rng ) X. ( U i^i Rng ) ) )
10	3	sqxpeqd	|- ( ph -> ( B X. B ) = ( ( U i^i Rng ) X. ( U i^i Rng ) ) )
11	10	eqcomd	|- ( ph -> ( ( U i^i Rng ) X. ( U i^i Rng ) ) = ( B X. B ) )
12	9 11	sylan9eqr	|- ( ( ph /\ u = U ) -> ( ( u i^i Rng ) X. ( u i^i Rng ) ) = ( B X. B ) )
13	12	reseq2d	|- ( ( ph /\ u = U ) -> ( RngHom |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) = ( RngHom |` ( B X. B ) ) )
14	4	eqcomd	|- ( ph -> ( RngHom |` ( B X. B ) ) = H )
15	14	adantr	|- ( ( ph /\ u = U ) -> ( RngHom |` ( B X. B ) ) = H )
16	13 15	eqtrd	|- ( ( ph /\ u = U ) -> ( RngHom |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) = H )
17	7 16	oveq12d	|- ( ( ph /\ u = U ) -> ( ( ExtStrCat ` u ) |`cat ( RngHom |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) ) = ( ( 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 -> ( RngCat ` U ) = ( ( ExtStrCat ` U ) |`cat H ) )
21	1 20	eqtrid	|- ( ph -> C = ( ( ExtStrCat ` U ) |`cat H ) )