rhmsubcsetclem1

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

Proof

Step	Hyp	Ref	Expression
1		rhmsubcsetc.c	$⊢ C = ExtStrCat (U)$
2		rhmsubcsetc.u	$⊢ φ \to U \in V$
3		rhmsubcsetc.b	$⊢ φ \to B = Ring \cap U$
4		rhmsubcsetc.h	$⊢ φ \to H = {RingHom ↾}_{(B \times B)}$
5	3	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in (Ring \cap U))$
6		elin	$⊢ x \in (Ring \cap U) \leftrightarrow (x \in Ring \land x \in U)$
7	6	simplbi	$⊢ x \in (Ring \cap U) \to x \in Ring$
8	5 7	syl6bi	$⊢ φ \to (x \in B \to x \in Ring)$
9	8	imp	$⊢ (φ \land x \in B) \to x \in Ring$
10		eqid	$⊢ {Base}_{x} = {Base}_{x}$
11	10	idrhm	$⊢ x \in Ring \to {I ↾}_{{Base}_{x}} \in (x RingHom x)$
12	9 11	syl	$⊢ (φ \land x \in B) \to {I ↾}_{{Base}_{x}} \in (x RingHom x)$
13		eqid	$⊢ Id (C) = Id (C)$
14	2	adantr	$⊢ (φ \land x \in B) \to U \in V$
15	6	simprbi	$⊢ x \in (Ring \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 ({RingHom ↾}_{(B \times B)}) x$
20		eqid	$⊢ RingCat (U) = RingCat (U)$
21		eqid	$⊢ {Base}_{RingCat (U)} = {Base}_{RingCat (U)}$
22		eqid	$⊢ Hom (RingCat (U)) = Hom (RingCat (U))$
23	20 21 2 22	ringchomfval	$⊢ φ \to Hom (RingCat (U)) = {RingHom ↾}_{({Base}_{RingCat (U)} \times {Base}_{RingCat (U)})}$
24	20 21 2	ringcbas	$⊢ φ \to {Base}_{RingCat (U)} = U \cap Ring$
25		incom	$⊢ Ring \cap U = U \cap Ring$
26	3 25	eqtrdi	$⊢ φ \to B = U \cap Ring$
27	26	eqcomd	$⊢ φ \to U \cap Ring = B$
28	24 27	eqtrd	$⊢ φ \to {Base}_{RingCat (U)} = B$
29	28	sqxpeqd	$⊢ φ \to {Base}_{RingCat (U)} \times {Base}_{RingCat (U)} = B \times B$
30	29	reseq2d	$⊢ φ \to {RingHom ↾}_{({Base}_{RingCat (U)} \times {Base}_{RingCat (U)})} = {RingHom ↾}_{(B \times B)}$
31	23 30	eqtrd	$⊢ φ \to Hom (RingCat (U)) = {RingHom ↾}_{(B \times B)}$
32	31	adantr	$⊢ (φ \land x \in B) \to Hom (RingCat (U)) = {RingHom ↾}_{(B \times B)}$
33	32	eqcomd	$⊢ (φ \land x \in B) \to {RingHom ↾}_{(B \times B)} = Hom (RingCat (U))$
34	33	oveqd	$⊢ (φ \land x \in B) \to x ({RingHom ↾}_{(B \times B)}) x = x Hom (RingCat (U)) x$
35	26	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in (U \cap Ring))$
36	35	biimpa	$⊢ (φ \land x \in B) \to x \in (U \cap Ring)$
37	24	adantr	$⊢ (φ \land x \in B) \to {Base}_{RingCat (U)} = U \cap Ring$
38	36 37	eleqtrrd	$⊢ (φ \land x \in B) \to x \in {Base}_{RingCat (U)}$
39	20 21 14 22 38 38	ringchom	$⊢ (φ \land x \in B) \to x Hom (RingCat (U)) x = x RingHom x$
40	19 34 39	3eqtrd	$⊢ (φ \land x \in B) \to x H x = x RingHom x$
41	12 18 40	3eltr4d	$⊢ (φ \land x \in B) \to Id (C) (x) \in (x H x)$

Metamath Proof Explorer

Theorem rhmsubcsetclem1

Proof