# 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 𝐶 = ( RingCat ‘ 𝑈 )
ringcid.b 𝐵 = ( Base ‘ 𝐶 )
ringcid.o 1 = ( Id ‘ 𝐶 )
ringcid.u ( 𝜑𝑈𝑉 )
ringcid.x ( 𝜑𝑋𝐵 )
ringcid.s 𝑆 = ( Base ‘ 𝑋 )
Assertion ringcid ( 𝜑 → ( 1𝑋 ) = ( I ↾ 𝑆 ) )

### Proof

Step Hyp Ref Expression
1 ringccat.c 𝐶 = ( RingCat ‘ 𝑈 )
2 ringcid.b 𝐵 = ( Base ‘ 𝐶 )
3 ringcid.o 1 = ( Id ‘ 𝐶 )
4 ringcid.u ( 𝜑𝑈𝑉 )
5 ringcid.x ( 𝜑𝑋𝐵 )
6 ringcid.s 𝑆 = ( Base ‘ 𝑋 )
7 eqidd ( 𝜑 → ( 𝑈 ∩ Ring ) = ( 𝑈 ∩ Ring ) )
8 eqidd ( 𝜑 → ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) = ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) )
9 1 4 7 8 ringcval ( 𝜑𝐶 = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) ) )
10 9 fveq2d ( 𝜑 → ( Id ‘ 𝐶 ) = ( Id ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) ) ) )
11 3 10 syl5eq ( 𝜑1 = ( Id ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) ) ) )
12 11 fveq1d ( 𝜑 → ( 1𝑋 ) = ( ( Id ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) ) ) ‘ 𝑋 ) )
13 eqid ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) ) = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) )
14 eqid ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 )
15 incom ( 𝑈 ∩ Ring ) = ( Ring ∩ 𝑈 )
16 15 a1i ( 𝜑 → ( 𝑈 ∩ Ring ) = ( Ring ∩ 𝑈 ) )
17 14 4 16 8 rhmsubcsetc ( 𝜑 → ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) ∈ ( Subcat ‘ ( ExtStrCat ‘ 𝑈 ) ) )
18 7 8 rhmresfn ( 𝜑 → ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) Fn ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) )
19 eqid ( Id ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( Id ‘ ( ExtStrCat ‘ 𝑈 ) )
20 1 2 4 ringcbas ( 𝜑𝐵 = ( 𝑈 ∩ Ring ) )
21 20 eleq2d ( 𝜑 → ( 𝑋𝐵𝑋 ∈ ( 𝑈 ∩ Ring ) ) )
22 5 21 mpbid ( 𝜑𝑋 ∈ ( 𝑈 ∩ Ring ) )
23 13 17 18 19 22 subcid ( 𝜑 → ( ( Id ‘ ( ExtStrCat ‘ 𝑈 ) ) ‘ 𝑋 ) = ( ( Id ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RingHom ↾ ( ( 𝑈 ∩ Ring ) × ( 𝑈 ∩ Ring ) ) ) ) ) ‘ 𝑋 ) )
24 elinel1 ( 𝑋 ∈ ( 𝑈 ∩ Ring ) → 𝑋𝑈 )
25 21 24 syl6bi ( 𝜑 → ( 𝑋𝐵𝑋𝑈 ) )
26 5 25 mpd ( 𝜑𝑋𝑈 )
27 14 19 4 26 estrcid ( 𝜑 → ( ( Id ‘ ( ExtStrCat ‘ 𝑈 ) ) ‘ 𝑋 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
28 6 eqcomi ( Base ‘ 𝑋 ) = 𝑆
29 28 a1i ( 𝜑 → ( Base ‘ 𝑋 ) = 𝑆 )
30 29 reseq2d ( 𝜑 → ( I ↾ ( Base ‘ 𝑋 ) ) = ( I ↾ 𝑆 ) )
31 27 30 eqtrd ( 𝜑 → ( ( Id ‘ ( ExtStrCat ‘ 𝑈 ) ) ‘ 𝑋 ) = ( I ↾ 𝑆 ) )
32 12 23 31 3eqtr2d ( 𝜑 → ( 1𝑋 ) = ( I ↾ 𝑆 ) )