Metamath Proof Explorer

Theorem rngchomfval

Description: Set of arrows 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 rngcbas.c 
|- C = ( RngCat ` U )
rngcbas.b 
|- B = ( Base ` C )
rngcbas.u 
|- ( ph -> U e. V )
rngchomfval.h 
|- H = ( Hom ` C )
Assertion rngchomfval 
|- ( ph -> H = ( RngHom |` ( B X. B ) ) )

Proof

Step Hyp Ref Expression
1 rngcbas.c 
 |-  C = ( RngCat ` U )
2 rngcbas.b 
 |-  B = ( Base ` C )
3 rngcbas.u 
 |-  ( ph -> U e. V )
4 rngchomfval.h 
 |-  H = ( Hom ` C )
5 1 2 3 rngcbas 
 |-  ( ph -> B = ( U i^i Rng ) )
6 eqidd 
 |-  ( ph -> ( RngHom |` ( B X. B ) ) = ( RngHom |` ( B X. B ) ) )
7 1 3 5 6 rngcval 
 |-  ( ph -> C = ( ( ExtStrCat ` U ) |`cat ( RngHom |` ( B X. B ) ) ) )
8 7 fveq2d 
 |-  ( ph -> ( Hom ` C ) = ( Hom ` ( ( ExtStrCat ` U ) |`cat ( RngHom |` ( B X. B ) ) ) ) )
9 4 8 eqtrid 
 |-  ( ph -> H = ( Hom ` ( ( ExtStrCat ` U ) |`cat ( RngHom |` ( B X. B ) ) ) ) )
10 eqid 
 |-  ( ( ExtStrCat ` U ) |`cat ( RngHom |` ( B X. B ) ) ) = ( ( ExtStrCat ` U ) |`cat ( RngHom |` ( B X. B ) ) )
11 eqid 
 |-  ( Base ` ( ExtStrCat ` U ) ) = ( Base ` ( ExtStrCat ` U ) )
12 fvexd 
 |-  ( ph -> ( ExtStrCat ` U ) e. _V )
13 5 6 rnghmresfn 
 |-  ( ph -> ( RngHom |` ( B X. B ) ) Fn ( B X. B ) )
14 inss1 
 |-  ( U i^i Rng ) C_ U
15 14 a1i 
 |-  ( ph -> ( U i^i Rng ) C_ U )
16 eqid 
 |-  ( ExtStrCat ` U ) = ( ExtStrCat ` U )
17 16 3 estrcbas 
 |-  ( ph -> U = ( Base ` ( ExtStrCat ` U ) ) )
18 17 eqcomd 
 |-  ( ph -> ( Base ` ( ExtStrCat ` U ) ) = U )
19 15 5 18 3sstr4d 
 |-  ( ph -> B C_ ( Base ` ( ExtStrCat ` U ) ) )
20 10 11 12 13 19 reschom 
 |-  ( ph -> ( RngHom |` ( B X. B ) ) = ( Hom ` ( ( ExtStrCat ` U ) |`cat ( RngHom |` ( B X. B ) ) ) ) )
21 9 20 eqtr4d 
 |-  ( ph -> H = ( RngHom |` ( B X. B ) ) )