Metamath Proof Explorer

Theorem rngcid

Description: The identity arrow in the category of non-unital rings is the identity function. (Contributed by AV, 27-Feb-2020) (Revised by AV, 10-Mar-2020)

Ref Expression
Hypotheses rngccat.c 
|- C = ( RngCat ` U )
rngcid.b 
|- B = ( Base ` C )
rngcid.o 
|- .1. = ( Id ` C )
rngcid.u 
|- ( ph -> U e. V )
rngcid.x 
|- ( ph -> X e. B )
rngcid.s 
|- S = ( Base ` X )
Assertion rngcid 
|- ( ph -> ( .1. ` X ) = ( _I |` S ) )

Proof

Step Hyp Ref Expression
1 rngccat.c 
 |-  C = ( RngCat ` U )
2 rngcid.b 
 |-  B = ( Base ` C )
3 rngcid.o 
 |-  .1. = ( Id ` C )
4 rngcid.u 
 |-  ( ph -> U e. V )
5 rngcid.x 
 |-  ( ph -> X e. B )
6 rngcid.s 
 |-  S = ( Base ` X )
7 eqidd 
 |-  ( ph -> ( U i^i Rng ) = ( U i^i Rng ) )
8 eqidd 
 |-  ( ph -> ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) = ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) )
9 1 4 7 8 rngcval 
 |-  ( ph -> C = ( ( ExtStrCat ` U ) |`cat ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) ) )
10 9 fveq2d 
 |-  ( ph -> ( Id ` C ) = ( Id ` ( ( ExtStrCat ` U ) |`cat ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) ) ) )
11 3 10 syl5eq 
 |-  ( ph -> .1. = ( Id ` ( ( ExtStrCat ` U ) |`cat ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) ) ) )
12 11 fveq1d 
 |-  ( ph -> ( .1. ` X ) = ( ( Id ` ( ( ExtStrCat ` U ) |`cat ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) ) ) ` X ) )
13 eqid 
 |-  ( ( ExtStrCat ` U ) |`cat ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) ) = ( ( ExtStrCat ` U ) |`cat ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) )
14 eqid 
 |-  ( ExtStrCat ` U ) = ( ExtStrCat ` U )
15 incom 
 |-  ( U i^i Rng ) = ( Rng i^i U )
16 15 a1i 
 |-  ( ph -> ( U i^i Rng ) = ( Rng i^i U ) )
17 14 4 16 8 rnghmsubcsetc 
 |-  ( ph -> ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) e. ( Subcat ` ( ExtStrCat ` U ) ) )
18 7 8 rnghmresfn 
 |-  ( ph -> ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) Fn ( ( U i^i Rng ) X. ( U i^i Rng ) ) )
19 eqid 
 |-  ( Id ` ( ExtStrCat ` U ) ) = ( Id ` ( ExtStrCat ` U ) )
20 1 2 4 rngcbas 
 |-  ( ph -> B = ( U i^i Rng ) )
21 20 eleq2d 
 |-  ( ph -> ( X e. B <-> X e. ( U i^i Rng ) ) )
22 5 21 mpbid 
 |-  ( ph -> X e. ( U i^i Rng ) )
23 13 17 18 19 22 subcid 
 |-  ( ph -> ( ( Id ` ( ExtStrCat ` U ) ) ` X ) = ( ( Id ` ( ( ExtStrCat ` U ) |`cat ( RngHomo |` ( ( U i^i Rng ) X. ( U i^i Rng ) ) ) ) ) ` X ) )
24 elinel1 
 |-  ( X e. ( U i^i Rng ) -> X e. U )
25 21 24 syl6bi 
 |-  ( ph -> ( X e. B -> X e. U ) )
26 5 25 mpd 
 |-  ( ph -> X e. U )
27 14 19 4 26 estrcid 
 |-  ( ph -> ( ( Id ` ( ExtStrCat ` U ) ) ` X ) = ( _I |` ( Base ` X ) ) )
28 6 eqcomi 
 |-  ( Base ` X ) = S
29 28 a1i 
 |-  ( ph -> ( Base ` X ) = S )
30 29 reseq2d 
 |-  ( ph -> ( _I |` ( Base ` X ) ) = ( _I |` S ) )
31 27 30 eqtrd 
 |-  ( ph -> ( ( Id ` ( ExtStrCat ` U ) ) ` X ) = ( _I |` S ) )
32 12 23 31 3eqtr2d 
 |-  ( ph -> ( .1. ` X ) = ( _I |` S ) )