Metamath Proof Explorer


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 = ( RngHomo |` ( 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 = ( RngHomo |` ( B X. B ) ) )
5 df-rngc
 |-  RngCat = ( u e. _V |-> ( ( ExtStrCat ` u ) |`cat ( RngHomo |` ( ( 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 ) -> ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) = ( RngHomo |` ( B X. B ) ) )
14 4 eqcomd
 |-  ( ph -> ( RngHomo |` ( B X. B ) ) = H )
15 14 adantr
 |-  ( ( ph /\ u = U ) -> ( RngHomo |` ( B X. B ) ) = H )
16 13 15 eqtrd
 |-  ( ( ph /\ u = U ) -> ( RngHomo |` ( ( u i^i Rng ) X. ( u i^i Rng ) ) ) = H )
17 7 16 oveq12d
 |-  ( ( ph /\ u = U ) -> ( ( ExtStrCat ` u ) |`cat ( RngHomo |` ( ( 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 syl5eq
 |-  ( ph -> C = ( ( ExtStrCat ` U ) |`cat H ) )