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

Proof

Step Hyp Ref Expression
1 rngccat.c ⊢ 𝐶 = ( RngCat ‘ 𝑈 )
2 rngcid.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
3 rngcid.o ⊢ 1 = ( Id ‘ 𝐶 )
4 rngcid.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑉 )
5 rngcid.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
6 rngcid.s ⊢ 𝑆 = ( Base ‘ 𝑋 )
7 eqidd ⊢ ( 𝜑 → ( 𝑈 ∩ Rng ) = ( 𝑈 ∩ Rng ) )
8 eqidd ⊢ ( 𝜑 → ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) = ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) )
9 1 4 7 8 rngcval ⊢ ( 𝜑 → 𝐶 = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ) )
10 9 fveq2d ⊢ ( 𝜑 → ( Id ‘ 𝐶 ) = ( Id ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ) ) )
11 3 10 syl5eq ⊢ ( 𝜑 → 1 = ( Id ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ) ) )
12 11 fveq1d ⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) = ( ( Id ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ) ) ‘ 𝑋 ) )
13 eqid ⊢ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ) = ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) )
14 eqid ⊢ ( ExtStrCat ‘ 𝑈 ) = ( ExtStrCat ‘ 𝑈 )
15 incom ⊢ ( 𝑈 ∩ Rng ) = ( Rng ∩ 𝑈 )
16 15 a1i ⊢ ( 𝜑 → ( 𝑈 ∩ Rng ) = ( Rng ∩ 𝑈 ) )
17 14 4 16 8 rnghmsubcsetc ⊢ ( 𝜑 → ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ∈ ( Subcat ‘ ( ExtStrCat ‘ 𝑈 ) ) )
18 7 8 rnghmresfn ⊢ ( 𝜑 → ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) Fn ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) )
19 eqid ⊢ ( Id ‘ ( ExtStrCat ‘ 𝑈 ) ) = ( Id ‘ ( ExtStrCat ‘ 𝑈 ) )
20 1 2 4 rngcbas ⊢ ( 𝜑 → 𝐵 = ( 𝑈 ∩ Rng ) )
21 20 eleq2d ⊢ ( 𝜑 → ( 𝑋 ∈ 𝐵 ↔ 𝑋 ∈ ( 𝑈 ∩ Rng ) ) )
22 5 21 mpbid ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑈 ∩ Rng ) )
23 13 17 18 19 22 subcid ⊢ ( 𝜑 → ( ( Id ‘ ( ExtStrCat ‘ 𝑈 ) ) ‘ 𝑋 ) = ( ( Id ‘ ( ( ExtStrCat ‘ 𝑈 ) ↾cat ( RngHomo ↾ ( ( 𝑈 ∩ Rng ) × ( 𝑈 ∩ Rng ) ) ) ) ) ‘ 𝑋 ) )
24 elinel1 ⊢ ( 𝑋 ∈ ( 𝑈 ∩ Rng ) → 𝑋 ∈ 𝑈 )
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 ↾ 𝑆 ) )