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	$$⊢C=\mathrm{RngCat}\left(U\right)$$
	rngcid.b	$$⊢B={\mathrm{Base}}_C$$
	rngcid.o	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	rngcid.u	$$⊢\phi \to U\in V$$
	rngcid.x	$$⊢\phi \to X\in B$$
	rngcid.s	$$⊢S={\mathrm{Base}}_X$$
Assertion	rngcid	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)={\mathrm{I}\upharpoonright }_S$$

Proof

Step	Hyp	Ref	Expression
1		rngccat.c	$$⊢C=\mathrm{RngCat}\left(U\right)$$
2		rngcid.b	$$⊢B={\mathrm{Base}}_C$$
3		rngcid.o	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
4		rngcid.u	$$⊢\phi \to U\in V$$
5		rngcid.x	$$⊢\phi \to X\in B$$
6		rngcid.s	$$⊢S={\mathrm{Base}}_X$$
7		eqidd	$$⊢\phi \to U\cap \mathrm{Rng}=U\cap \mathrm{Rng}$$
8		eqidd	$$⊢\phi \to {\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}={\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}$$
9	1 4 7 8	rngcval	$$⊢\phi \to C=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\right)$$
10	9	fveq2d	$$⊢\phi \to \mathrm{Id}\left(C\right)=\mathrm{Id}\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\right)\right)$$
11	3 10	syl5eq	$$⊢\phi \to \underset{\dot{}}{1}=\mathrm{Id}\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\right)\right)$$
12	11	fveq1d	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)=\mathrm{Id}\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\right)\right)\left(X\right)$$
13		eqid	$$⊢\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\right)=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\right)$$
14		eqid	$$⊢\mathrm{ExtStrCat}\left(U\right)=\mathrm{ExtStrCat}\left(U\right)$$
15		incom	$$⊢U\cap \mathrm{Rng}=\mathrm{Rng}\cap U$$
16	15	a1i	$$⊢\phi \to U\cap \mathrm{Rng}=\mathrm{Rng}\cap U$$
17	14 4 16 8	rnghmsubcsetc	$$⊢\phi \to {\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\in \mathrm{Subcat}\left(\mathrm{ExtStrCat}\left(U\right)\right)$$
18	7 8	rnghmresfn	$$⊢\phi \to \left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\right)Fn\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)$$
19		eqid	$$⊢\mathrm{Id}\left(\mathrm{ExtStrCat}\left(U\right)\right)=\mathrm{Id}\left(\mathrm{ExtStrCat}\left(U\right)\right)$$
20	1 2 4	rngcbas	$$⊢\phi \to B=U\cap \mathrm{Rng}$$
21	20	eleq2d	$$⊢\phi \to \left(X\in B\leftrightarrow X\in \left(U\cap \mathrm{Rng}\right)\right)$$
22	5 21	mpbid	$$⊢\phi \to X\in \left(U\cap \mathrm{Rng}\right)$$
23	13 17 18 19 22	subcid	$$⊢\phi \to \mathrm{Id}\left(\mathrm{ExtStrCat}\left(U\right)\right)\left(X\right)=\mathrm{Id}\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RngHomo}\upharpoonright }_{\left(\left(U\cap \mathrm{Rng}\right)\times \left(U\cap \mathrm{Rng}\right)\right)}\right)\right)\left(X\right)$$
24		elinel1	$$⊢X\in \left(U\cap \mathrm{Rng}\right)\to X\in U$$
25	21 24	syl6bi	$$⊢\phi \to \left(X\in B\to X\in U\right)$$
26	5 25	mpd	$$⊢\phi \to X\in U$$
27	14 19 4 26	estrcid	$$⊢\phi \to \mathrm{Id}\left(\mathrm{ExtStrCat}\left(U\right)\right)\left(X\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
28	6	eqcomi	$$⊢{\mathrm{Base}}_X=S$$
29	28	a1i	$$⊢\phi \to {\mathrm{Base}}_X=S$$
30	29	reseq2d	$$⊢\phi \to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}={\mathrm{I}\upharpoonright }_S$$
31	27 30	eqtrd	$$⊢\phi \to \mathrm{Id}\left(\mathrm{ExtStrCat}\left(U\right)\right)\left(X\right)={\mathrm{I}\upharpoonright }_S$$
32	12 23 31	3eqtr2d	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)={\mathrm{I}\upharpoonright }_S$$