Metamath Proof Explorer

Theorem ringcid

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

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

Proof

Step Hyp Ref Expression
1 ringccat.c 
 |-  C = ( RingCat ` U )
2 ringcid.b 
 |-  B = ( Base ` C )
3 ringcid.o 
 |-  .1. = ( Id ` C )
4 ringcid.u 
 |-  ( ph -> U e. V )
5 ringcid.x 
 |-  ( ph -> X e. B )
6 ringcid.s 
 |-  S = ( Base ` X )
7 eqidd 
 |-  ( ph -> ( U i^i Ring ) = ( U i^i Ring ) )
8 eqidd 
 |-  ( ph -> ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) = ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) )
9 1 4 7 8 ringcval 
 |-  ( ph -> C = ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) ) )
10 9 fveq2d 
 |-  ( ph -> ( Id ` C ) = ( Id ` ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) ) ) )
11 3 10 syl5eq 
 |-  ( ph -> .1. = ( Id ` ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) ) ) )
12 11 fveq1d 
 |-  ( ph -> ( .1. ` X ) = ( ( Id ` ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) ) ) ` X ) )
13 eqid 
 |-  ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) ) = ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) )
14 eqid 
 |-  ( ExtStrCat ` U ) = ( ExtStrCat ` U )
15 incom 
 |-  ( U i^i Ring ) = ( Ring i^i U )
16 15 a1i 
 |-  ( ph -> ( U i^i Ring ) = ( Ring i^i U ) )
17 14 4 16 8 rhmsubcsetc 
 |-  ( ph -> ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) e. ( Subcat ` ( ExtStrCat ` U ) ) )
18 7 8 rhmresfn 
 |-  ( ph -> ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) Fn ( ( U i^i Ring ) X. ( U i^i Ring ) ) )
19 eqid 
 |-  ( Id ` ( ExtStrCat ` U ) ) = ( Id ` ( ExtStrCat ` U ) )
20 1 2 4 ringcbas 
 |-  ( ph -> B = ( U i^i Ring ) )
21 20 eleq2d 
 |-  ( ph -> ( X e. B <-> X e. ( U i^i Ring ) ) )
22 5 21 mpbid 
 |-  ( ph -> X e. ( U i^i Ring ) )
23 13 17 18 19 22 subcid 
 |-  ( ph -> ( ( Id ` ( ExtStrCat ` U ) ) ` X ) = ( ( Id ` ( ( ExtStrCat ` U ) |`cat ( RingHom |` ( ( U i^i Ring ) X. ( U i^i Ring ) ) ) ) ) ` X ) )
24 elinel1 
 |-  ( X e. ( U i^i Ring ) -> 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 ) )