Theorem funcringcsetclem7ALTV

Description: Lemma 7 for funcringcsetcALTV . (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	funcringcsetcALTV.r	$$⊢R=\mathrm{RingCatALTV}\left(U\right)$$
	funcringcsetcALTV.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
	funcringcsetcALTV.b	$$⊢B={\mathrm{Base}}_R$$
	funcringcsetcALTV.c	$$⊢C={\mathrm{Base}}_S$$
	funcringcsetcALTV.u	$$⊢\phi \to U\in \mathrm{WUni}$$
	funcringcsetcALTV.f	$$⊢\phi \to F=\left(x\in B⟼{\mathrm{Base}}_x\right)$$
	funcringcsetcALTV.g	$$⊢\phi \to G=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}\right)$$
Assertion	funcringcsetclem7ALTV	$$⊢\left(\phi \wedge X\in B\right)\to \left(XGX\right)\left(\mathrm{Id}\left(R\right)\left(X\right)\right)=\mathrm{Id}\left(S\right)\left(F\left(X\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		funcringcsetcALTV.r	$$⊢R=\mathrm{RingCatALTV}\left(U\right)$$
2		funcringcsetcALTV.s	$$⊢S=\mathrm{SetCat}\left(U\right)$$
3		funcringcsetcALTV.b	$$⊢B={\mathrm{Base}}_R$$
4		funcringcsetcALTV.c	$$⊢C={\mathrm{Base}}_S$$
5		funcringcsetcALTV.u	$$⊢\phi \to U\in \mathrm{WUni}$$
6		funcringcsetcALTV.f	$$⊢\phi \to F=\left(x\in B⟼{\mathrm{Base}}_x\right)$$
7		funcringcsetcALTV.g	$$⊢\phi \to G=\left(x\in B,y\in B⟼{\mathrm{I}\upharpoonright }_{\left(x\mathrm{RingHom}y\right)}\right)$$
8	1 2 3 4 5 6 7	funcringcsetclem5ALTV	$$⊢\left(\phi \wedge \left(X\in B\wedge X\in B\right)\right)\to XGX={\mathrm{I}\upharpoonright }_{\left(X\mathrm{RingHom}X\right)}$$
9	8	anabsan2	$$⊢\left(\phi \wedge X\in B\right)\to XGX={\mathrm{I}\upharpoonright }_{\left(X\mathrm{RingHom}X\right)}$$
10		eqid	$$⊢\mathrm{Id}\left(R\right)=\mathrm{Id}\left(R\right)$$
11	5	adantr	$$⊢\left(\phi \wedge X\in B\right)\to U\in \mathrm{WUni}$$
12		simpr	$$⊢\left(\phi \wedge X\in B\right)\to X\in B$$
13		eqid	$$⊢{\mathrm{Base}}_X={\mathrm{Base}}_X$$
14	1 3 10 11 12 13	ringcidALTV	$$⊢\left(\phi \wedge X\in B\right)\to \mathrm{Id}\left(R\right)\left(X\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
15	9 14	fveq12d	$$⊢\left(\phi \wedge X\in B\right)\to \left(XGX\right)\left(\mathrm{Id}\left(R\right)\left(X\right)\right)=\left({\mathrm{I}\upharpoonright }_{\left(X\mathrm{RingHom}X\right)}\right)\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\right)$$
16	1 3 5	ringcbasALTV	$$⊢\phi \to B=U\cap \mathrm{Ring}$$
17	16	eleq2d	$$⊢\phi \to \left(X\in B\leftrightarrow X\in \left(U\cap \mathrm{Ring}\right)\right)$$
18		elin	$$⊢X\in \left(U\cap \mathrm{Ring}\right)\leftrightarrow \left(X\in U\wedge X\in \mathrm{Ring}\right)$$
19	18	simprbi	$$⊢X\in \left(U\cap \mathrm{Ring}\right)\to X\in \mathrm{Ring}$$
20	17 19	syl6bi	$$⊢\phi \to \left(X\in B\to X\in \mathrm{Ring}\right)$$
21	20	imp	$$⊢\left(\phi \wedge X\in B\right)\to X\in \mathrm{Ring}$$
22	13	idrhm	$$⊢X\in \mathrm{Ring}\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\in \left(X\mathrm{RingHom}X\right)$$
23		fvresi	$$⊢{\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\in \left(X\mathrm{RingHom}X\right)\to \left({\mathrm{I}\upharpoonright }_{\left(X\mathrm{RingHom}X\right)}\right)\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
24	21 22 23	3syl	$$⊢\left(\phi \wedge X\in B\right)\to \left({\mathrm{I}\upharpoonright }_{\left(X\mathrm{RingHom}X\right)}\right)\left({\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
25	1 2 3 4 5 6	funcringcsetclem1ALTV	$$⊢\left(\phi \wedge X\in B\right)\to F\left(X\right)={\mathrm{Base}}_X$$
26	25	fveq2d	$$⊢\left(\phi \wedge X\in B\right)\to \mathrm{Id}\left(S\right)\left(F\left(X\right)\right)=\mathrm{Id}\left(S\right)\left({\mathrm{Base}}_X\right)$$
27		eqid	$$⊢\mathrm{Id}\left(S\right)=\mathrm{Id}\left(S\right)$$
28	1 3 5	ringcbasbasALTV	$$⊢\left(\phi \wedge X\in B\right)\to {\mathrm{Base}}_X\in U$$
29	2 27 11 28	setcid	$$⊢\left(\phi \wedge X\in B\right)\to \mathrm{Id}\left(S\right)\left({\mathrm{Base}}_X\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}$$
30	26 29	eqtr2d	$$⊢\left(\phi \wedge X\in B\right)\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_X}=\mathrm{Id}\left(S\right)\left(F\left(X\right)\right)$$
31	15 24 30	3eqtrd	$$⊢\left(\phi \wedge X\in B\right)\to \left(XGX\right)\left(\mathrm{Id}\left(R\right)\left(X\right)\right)=\mathrm{Id}\left(S\right)\left(F\left(X\right)\right)$$