rnghmsubcsetclem1

	Ref	Expression
Hypotheses	rnghmsubcsetc.c	$⊢ C = ExtStrCat (U)$
	rnghmsubcsetc.u	$⊢ φ \to U \in V$
	rnghmsubcsetc.b	$⊢ φ \to B = Rng \cap U$
	rnghmsubcsetc.h	$⊢ φ \to H = {RngHom ↾}_{(B \times B)}$
Assertion	rnghmsubcsetclem1	$⊢ (φ \land x \in B) \to Id (C) (x) \in (x H x)$

Proof

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

Metamath Proof Explorer

Theorem rnghmsubcsetclem1

Proof