Theorem ringcidALTV

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

	Ref	Expression
Hypotheses	ringccatALTV.c	|- C = ( RingCatALTV ` U )
	ringcidALTV.b	|- B = ( Base ` C )
	ringcidALTV.o	|- .1. = ( Id ` C )
	ringcidALTV.u	|- ( ph -> U e. V )
	ringcidALTV.x	|- ( ph -> X e. B )
	ringcidALTV.s	|- S = ( Base ` X )
Assertion	ringcidALTV	|- ( ph -> ( .1. ` X ) = ( _I |` S ) )

Proof

Step	Hyp	Ref	Expression
1		ringccatALTV.c	|- C = ( RingCatALTV ` U )
2		ringcidALTV.b	|- B = ( Base ` C )
3		ringcidALTV.o	|- .1. = ( Id ` C )
4		ringcidALTV.u	|- ( ph -> U e. V )
5		ringcidALTV.x	|- ( ph -> X e. B )
6		ringcidALTV.s	|- S = ( Base ` X )
7	1 2	ringccatidALTV	|- ( 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 ) )