rhmsubclem3

	Ref	Expression
Hypotheses	rngcrescrhm.u	$⊢ φ \to U \in V$
	rngcrescrhm.c	$⊢ C = RngCat (U)$
	rngcrescrhm.r	$⊢ φ \to R = Ring \cap U$
	rngcrescrhm.h	$⊢ H = {RingHom ↾}_{(R \times R)}$
Assertion	rhmsubclem3	$⊢ (φ \land x \in R) \to Id (RngCat (U)) (x) \in (x H x)$

Step	Hyp	Ref	Expression
1		rngcrescrhm.u	$⊢ φ \to U \in V$
2		rngcrescrhm.c	$⊢ C = RngCat (U)$
3		rngcrescrhm.r	$⊢ φ \to R = Ring \cap U$
4		rngcrescrhm.h	$⊢ H = {RingHom ↾}_{(R \times R)}$
5	3	eleq2d	$⊢ φ \to (x \in R \leftrightarrow x \in (Ring \cap U))$
6		elinel1	$⊢ x \in (Ring \cap U) \to x \in Ring$
7	5 6	syl6bi	$⊢ φ \to (x \in R \to x \in Ring)$
8	7	imp	$⊢ (φ \land x \in R) \to x \in Ring$
9		eqid	$⊢ {Base}_{x} = {Base}_{x}$
10	9	idrhm	$⊢ x \in Ring \to {I ↾}_{{Base}_{x}} \in (x RingHom x)$
11	8 10	syl	$⊢ (φ \land x \in R) \to {I ↾}_{{Base}_{x}} \in (x RingHom x)$
12		eqid	$⊢ {Base}_{C} = {Base}_{C}$
13	2	eqcomi	$⊢ RngCat (U) = C$
14	13	fveq2i	$⊢ Id (RngCat (U)) = Id (C)$
15	1	adantr	$⊢ (φ \land x \in R) \to U \in V$
16		incom	$⊢ Ring \cap U = U \cap Ring$
17		ringssrng	$⊢ Ring \subseteq Rng$
18		sslin	$⊢ Ring \subseteq Rng \to U \cap Ring \subseteq U \cap Rng$
19	17 18	mp1i	$⊢ φ \to U \cap Ring \subseteq U \cap Rng$
20	16 19	eqsstrid	$⊢ φ \to Ring \cap U \subseteq U \cap Rng$
21	2 12 1	rngcbas	$⊢ φ \to {Base}_{C} = U \cap Rng$
22	20 3 21	3sstr4d	$⊢ φ \to R \subseteq {Base}_{C}$
23	22	sselda	$⊢ (φ \land x \in R) \to x \in {Base}_{C}$
24	2 12 14 15 23 9	rngcid	$⊢ (φ \land x \in R) \to Id (RngCat (U)) (x) = {I ↾}_{{Base}_{x}}$
25	1 2 3 4	rhmsubclem2	$⊢ (φ \land x \in R \land x \in R) \to x H x = x RingHom x$
26	25	3anidm23	$⊢ (φ \land x \in R) \to x H x = x RingHom x$
27	11 24 26	3eltr4d	$⊢ (φ \land x \in R) \to Id (RngCat (U)) (x) \in (x H x)$

Metamath Proof Explorer