Theorem ringcid

Description: The identity arrow in the category of unital rings is the identity function. (Contributed by AV, 14-Feb-2020) (Revised by AV, 10-Mar-2020)

	Ref	Expression
Hypotheses	ringccat.c	$$⊢C=\mathrm{RingCat}\left(U\right)$$
	ringcid.b	$$⊢B={\mathrm{Base}}_C$$
	ringcid.o	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
	ringcid.u	$$⊢\phi \to U\in V$$
	ringcid.x	$$⊢\phi \to X\in B$$
	ringcid.s	$$⊢S={\mathrm{Base}}_X$$
Assertion	ringcid	$$⊢\phi \to \underset{\dot{}}{1}\left(X\right)={\mathrm{I}\upharpoonright }_S$$

Proof

Step	Hyp	Ref	Expression
1		ringccat.c	$$⊢C=\mathrm{RingCat}\left(U\right)$$
2		ringcid.b	$$⊢B={\mathrm{Base}}_C$$
3		ringcid.o	$$⊢\underset{\dot{}}{1}=\mathrm{Id}\left(C\right)$$
4		ringcid.u	$$⊢\phi \to U\in V$$
5		ringcid.x	$$⊢\phi \to X\in B$$
6		ringcid.s	$$⊢S={\mathrm{Base}}_X$$
7		eqidd	$$⊢\phi \to U\cap \mathrm{Ring}=U\cap \mathrm{Ring}$$
8		eqidd	$$⊢\phi \to {\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}={\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}$$
9	1 4 7 8	ringcval	$$⊢\phi \to C=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\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{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}\right)\right)$$
11	3 10	eqtrid	$$⊢\phi \to \underset{\dot{}}{1}=\mathrm{Id}\left(\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\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{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}\right)\right)\left(X\right)$$
13		eqid	$$⊢\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}\right)=\mathrm{ExtStrCat}\left(U\right){\upharpoonright }_{\mathrm{cat}}\left({\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}\right)$$
14		eqid	$$⊢\mathrm{ExtStrCat}\left(U\right)=\mathrm{ExtStrCat}\left(U\right)$$
15		incom	$$⊢U\cap \mathrm{Ring}=\mathrm{Ring}\cap U$$
16	15	a1i	$$⊢\phi \to U\cap \mathrm{Ring}=\mathrm{Ring}\cap U$$
17	14 4 16 8	rhmsubcsetc	$$⊢\phi \to {\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}\in \mathrm{Subcat}\left(\mathrm{ExtStrCat}\left(U\right)\right)$$
18	7 8	rhmresfn	$$⊢\phi \to \left({\mathrm{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}\right)Fn\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\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	ringcbas	$$⊢\phi \to B=U\cap \mathrm{Ring}$$
21	20	eleq2d	$$⊢\phi \to \left(X\in B\leftrightarrow X\in \left(U\cap \mathrm{Ring}\right)\right)$$
22	5 21	mpbid	$$⊢\phi \to X\in \left(U\cap \mathrm{Ring}\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{RingHom}\upharpoonright }_{\left(\left(U\cap \mathrm{Ring}\right)\times \left(U\cap \mathrm{Ring}\right)\right)}\right)\right)\left(X\right)$$
24		elinel1	$$⊢X\in \left(U\cap \mathrm{Ring}\right)\to X\in U$$
25	21 24	biimtrdi	$$⊢\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$$