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 eqtrid ⊢ ( 𝜑 → 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 biimtrdi ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 → 𝑋 ∈ 𝑈 ) )
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 ↾ 𝑆 ) )