Metamath Proof Explorer


Theorem rngcidALTV

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

Ref Expression
Hypotheses rngccatALTV.c 𝐶 = ( RngCatALTV ‘ 𝑈 )
rngcidALTV.b 𝐵 = ( Base ‘ 𝐶 )
rngcidALTV.o 1 = ( Id ‘ 𝐶 )
rngcidALTV.u ( 𝜑𝑈𝑉 )
rngcidALTV.x ( 𝜑𝑋𝐵 )
rngcidALTV.s 𝑆 = ( Base ‘ 𝑋 )
Assertion rngcidALTV ( 𝜑 → ( 1𝑋 ) = ( I ↾ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 rngccatALTV.c 𝐶 = ( RngCatALTV ‘ 𝑈 )
2 rngcidALTV.b 𝐵 = ( Base ‘ 𝐶 )
3 rngcidALTV.o 1 = ( Id ‘ 𝐶 )
4 rngcidALTV.u ( 𝜑𝑈𝑉 )
5 rngcidALTV.x ( 𝜑𝑋𝐵 )
6 rngcidALTV.s 𝑆 = ( Base ‘ 𝑋 )
7 1 2 rngccatidALTV ( 𝑈𝑉 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥𝐵 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) )
8 4 7 syl ( 𝜑 → ( 𝐶 ∈ Cat ∧ ( Id ‘ 𝐶 ) = ( 𝑥𝐵 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) ) )
9 8 simprd ( 𝜑 → ( Id ‘ 𝐶 ) = ( 𝑥𝐵 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) )
10 3 9 syl5eq ( 𝜑1 = ( 𝑥𝐵 ↦ ( I ↾ ( Base ‘ 𝑥 ) ) ) )
11 fveq2 ( 𝑥 = 𝑋 → ( Base ‘ 𝑥 ) = ( Base ‘ 𝑋 ) )
12 11 adantl ( ( 𝜑𝑥 = 𝑋 ) → ( Base ‘ 𝑥 ) = ( Base ‘ 𝑋 ) )
13 12 reseq2d ( ( 𝜑𝑥 = 𝑋 ) → ( I ↾ ( Base ‘ 𝑥 ) ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
14 fvex ( Base ‘ 𝑋 ) ∈ V
15 resiexg ( ( Base ‘ 𝑋 ) ∈ V → ( I ↾ ( Base ‘ 𝑋 ) ) ∈ V )
16 14 15 mp1i ( 𝜑 → ( I ↾ ( Base ‘ 𝑋 ) ) ∈ V )
17 10 13 5 16 fvmptd ( 𝜑 → ( 1𝑋 ) = ( I ↾ ( Base ‘ 𝑋 ) ) )
18 6 reseq2i ( I ↾ 𝑆 ) = ( I ↾ ( Base ‘ 𝑋 ) )
19 17 18 eqtr4di ( 𝜑 → ( 1𝑋 ) = ( I ↾ 𝑆 ) )