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	|- C = ( RngCatALTV ` U )
	rngcidALTV.b	|- B = ( Base ` C )
	rngcidALTV.o	|- .1. = ( Id ` C )
	rngcidALTV.u	|- ( ph -> U e. V )
	rngcidALTV.x	|- ( ph -> X e. B )
	rngcidALTV.s	|- S = ( Base ` X )
Assertion	rngcidALTV	|- ( ph -> ( .1. ` X ) = ( _I |` S ) )

Proof

Step	Hyp	Ref	Expression
1		rngccatALTV.c	|- C = ( RngCatALTV ` U )
2		rngcidALTV.b	|- B = ( Base ` C )
3		rngcidALTV.o	|- .1. = ( Id ` C )
4		rngcidALTV.u	|- ( ph -> U e. V )
5		rngcidALTV.x	|- ( ph -> X e. B )
6		rngcidALTV.s	|- S = ( Base ` X )
7	1 2	rngccatidALTV	|- ( U e. V -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( _I |` ( Base ` x ) ) ) ) )
8	4 7	syl	|- ( ph -> ( C e. Cat /\ ( Id ` C ) = ( x e. B |-> ( _I |` ( Base ` x ) ) ) ) )
9	8	simprd	|- ( ph -> ( Id ` C ) = ( x e. B |-> ( _I |` ( Base ` x ) ) ) )
10	3 9	eqtrid	|- ( ph -> .1. = ( x e. B |-> ( _I |` ( Base ` x ) ) ) )
11		fveq2	|- ( x = X -> ( Base ` x ) = ( Base ` X ) )
12	11	adantl	|- ( ( ph /\ x = X ) -> ( Base ` x ) = ( Base ` X ) )
13	12	reseq2d	|- ( ( ph /\ x = X ) -> ( _I |` ( Base ` x ) ) = ( _I |` ( Base ` X ) ) )
14		fvex	|- ( Base ` X ) e. _V
15		resiexg	|- ( ( Base ` X ) e. _V -> ( _I |` ( Base ` X ) ) e. _V )
16	14 15	mp1i	|- ( ph -> ( _I |` ( Base ` X ) ) e. _V )
17	10 13 5 16	fvmptd	|- ( ph -> ( .1. ` X ) = ( _I |` ( Base ` X ) ) )
18	6	reseq2i	|- ( _I |` S ) = ( _I |` ( Base ` X ) )
19	17 18	eqtr4di	|- ( ph -> ( .1. ` X ) = ( _I |` S ) )