Theorem rnghmsubcsetclem1

Description: Lemma 1 for rnghmsubcsetc . (Contributed by AV, 9-Mar-2020)

	Ref	Expression
Hypotheses	rnghmsubcsetc.c	$$⊢C=\mathrm{ExtStrCat}\left(U\right)$$
	rnghmsubcsetc.u	$$⊢\phi \to U\in V$$
	rnghmsubcsetc.b	$$⊢\phi \to B=\mathrm{Rng}\cap U$$
	rnghmsubcsetc.h	$$⊢\phi \to H={\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}$$
Assertion	rnghmsubcsetclem1	$$⊢\left(\phi \wedge x\in B\right)\to \mathrm{Id}\left(C\right)\left(x\right)\in \left(xHx\right)$$

Proof

Step	Hyp	Ref	Expression
1		rnghmsubcsetc.c	$$⊢C=\mathrm{ExtStrCat}\left(U\right)$$
2		rnghmsubcsetc.u	$$⊢\phi \to U\in V$$
3		rnghmsubcsetc.b	$$⊢\phi \to B=\mathrm{Rng}\cap U$$
4		rnghmsubcsetc.h	$$⊢\phi \to H={\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}$$
5	3	eleq2d	$$⊢\phi \to \left(x\in B\leftrightarrow x\in \left(\mathrm{Rng}\cap U\right)\right)$$
6		elin	$$⊢x\in \left(\mathrm{Rng}\cap U\right)\leftrightarrow \left(x\in \mathrm{Rng}\wedge x\in U\right)$$
7	6	simplbi	$$⊢x\in \left(\mathrm{Rng}\cap U\right)\to x\in \mathrm{Rng}$$
8	5 7	syl6bi	$$⊢\phi \to \left(x\in B\to x\in \mathrm{Rng}\right)$$
9	8	imp	$$⊢\left(\phi \wedge x\in B\right)\to x\in \mathrm{Rng}$$
10		eqid	$$⊢{\mathrm{Base}}_x={\mathrm{Base}}_x$$
11	10	idrnghm	$$⊢x\in \mathrm{Rng}\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}\in \left(x\mathrm{RngHomo}x\right)$$
12	9 11	syl	$$⊢\left(\phi \wedge x\in B\right)\to {\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}\in \left(x\mathrm{RngHomo}x\right)$$
13		eqid	$$⊢\mathrm{Id}\left(C\right)=\mathrm{Id}\left(C\right)$$
14	2	adantr	$$⊢\left(\phi \wedge x\in B\right)\to U\in V$$
15	6	simprbi	$$⊢x\in \left(\mathrm{Rng}\cap U\right)\to x\in U$$
16	5 15	syl6bi	$$⊢\phi \to \left(x\in B\to x\in U\right)$$
17	16	imp	$$⊢\left(\phi \wedge x\in B\right)\to x\in U$$
18	1 13 14 17	estrcid	$$⊢\left(\phi \wedge x\in B\right)\to \mathrm{Id}\left(C\right)\left(x\right)={\mathrm{I}\upharpoonright }_{{\mathrm{Base}}_x}$$
19	4	oveqdr	$$⊢\left(\phi \wedge x\in B\right)\to xHx=x\left({\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}\right)x$$
20		eqid	$$⊢\mathrm{RngCat}\left(U\right)=\mathrm{RngCat}\left(U\right)$$
21		eqid	$$⊢{\mathrm{Base}}_{\mathrm{RngCat}\left(U\right)}={\mathrm{Base}}_{\mathrm{RngCat}\left(U\right)}$$
22		eqid	$$⊢\mathrm{Hom}\left(\mathrm{RngCat}\left(U\right)\right)=\mathrm{Hom}\left(\mathrm{RngCat}\left(U\right)\right)$$
23	20 21 2 22	rngchomfval	$$⊢\phi \to \mathrm{Hom}\left(\mathrm{RngCat}\left(U\right)\right)={\mathrm{RngHomo}\upharpoonright }_{\left({\mathrm{Base}}_{\mathrm{RngCat}\left(U\right)}\times {\mathrm{Base}}_{\mathrm{RngCat}\left(U\right)}\right)}$$
24	20 21 2	rngcbas	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{RngCat}\left(U\right)}=U\cap \mathrm{Rng}$$
25		incom	$$⊢\mathrm{Rng}\cap U=U\cap \mathrm{Rng}$$
26	3 25	eqtrdi	$$⊢\phi \to B=U\cap \mathrm{Rng}$$
27	26	eqcomd	$$⊢\phi \to U\cap \mathrm{Rng}=B$$
28	24 27	eqtrd	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{RngCat}\left(U\right)}=B$$
29	28	sqxpeqd	$$⊢\phi \to {\mathrm{Base}}_{\mathrm{RngCat}\left(U\right)}\times {\mathrm{Base}}_{\mathrm{RngCat}\left(U\right)}=B\times B$$
30	29	reseq2d	$$⊢\phi \to {\mathrm{RngHomo}\upharpoonright }_{\left({\mathrm{Base}}_{\mathrm{RngCat}\left(U\right)}\times {\mathrm{Base}}_{\mathrm{RngCat}\left(U\right)}\right)}={\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}$$
31	23 30	eqtrd	$$⊢\phi \to \mathrm{Hom}\left(\mathrm{RngCat}\left(U\right)\right)={\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}$$
32	31	adantr	$$⊢\left(\phi \wedge x\in B\right)\to \mathrm{Hom}\left(\mathrm{RngCat}\left(U\right)\right)={\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}$$
33	32	eqcomd	$$⊢\left(\phi \wedge x\in B\right)\to {\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}=\mathrm{Hom}\left(\mathrm{RngCat}\left(U\right)\right)$$
34	33	oveqd	$$⊢\left(\phi \wedge x\in B\right)\to x\left({\mathrm{RngHomo}\upharpoonright }_{\left(B\times B\right)}\right)x=x\mathrm{Hom}\left(\mathrm{RngCat}\left(U\right)\right)x$$
35	26	eleq2d	$$⊢\phi \to \left(x\in B\leftrightarrow x\in \left(U\cap \mathrm{Rng}\right)\right)$$
36	35	biimpa	$$⊢\left(\phi \wedge x\in B\right)\to x\in \left(U\cap \mathrm{Rng}\right)$$
37	24	adantr	$$⊢\left(\phi \wedge x\in B\right)\to {\mathrm{Base}}_{\mathrm{RngCat}\left(U\right)}=U\cap \mathrm{Rng}$$
38	36 37	eleqtrrd	$$⊢\left(\phi \wedge x\in B\right)\to x\in {\mathrm{Base}}_{\mathrm{RngCat}\left(U\right)}$$
39	20 21 14 22 38 38	rngchom	$$⊢\left(\phi \wedge x\in B\right)\to x\mathrm{Hom}\left(\mathrm{RngCat}\left(U\right)\right)x=x\mathrm{RngHomo}x$$
40	19 34 39	3eqtrd	$$⊢\left(\phi \wedge x\in B\right)\to xHx=x\mathrm{RngHomo}x$$
41	12 18 40	3eltr4d	$$⊢\left(\phi \wedge x\in B\right)\to \mathrm{Id}\left(C\right)\left(x\right)\in \left(xHx\right)$$