rhmsubcrngclem1

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

Proof

Step	Hyp	Ref	Expression
1		rhmsubcrngc.c	$⊢ C = RngCat (U)$
2		rhmsubcrngc.u	$⊢ φ \to U \in V$
3		rhmsubcrngc.b	$⊢ φ \to B = Ring \cap U$
4		rhmsubcrngc.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	$⊢ {Base}_{C} = {Base}_{C}$
14		eqid	$⊢ Id (C) = Id (C)$
15	2	adantr	$⊢ (φ \land x \in B) \to U \in V$
16		ringrng	$⊢ x \in Ring \to x \in Rng$
17	16	anim2i	$⊢ (x \in U \land x \in Ring) \to (x \in U \land x \in Rng)$
18	17	ancoms	$⊢ (x \in Ring \land x \in U) \to (x \in U \land x \in Rng)$
19	6 18	sylbi	$⊢ x \in (Ring \cap U) \to (x \in U \land x \in Rng)$
20	19	adantl	$⊢ (φ \land x \in (Ring \cap U)) \to (x \in U \land x \in Rng)$
21		elin	$⊢ x \in (U \cap Rng) \leftrightarrow (x \in U \land x \in Rng)$
22	20 21	sylibr	$⊢ (φ \land x \in (Ring \cap U)) \to x \in (U \cap Rng)$
23	1 13 2	rngcbas	$⊢ φ \to {Base}_{C} = U \cap Rng$
24	23	adantr	$⊢ (φ \land x \in (Ring \cap U)) \to {Base}_{C} = U \cap Rng$
25	22 24	eleqtrrd	$⊢ (φ \land x \in (Ring \cap U)) \to x \in {Base}_{C}$
26	25	ex	$⊢ φ \to (x \in (Ring \cap U) \to x \in {Base}_{C})$
27	5 26	sylbid	$⊢ φ \to (x \in B \to x \in {Base}_{C})$
28	27	imp	$⊢ (φ \land x \in B) \to x \in {Base}_{C}$
29	1 13 14 15 28 10	rngcid	$⊢ (φ \land x \in B) \to Id (C) (x) = {I ↾}_{{Base}_{x}}$
30	4	oveqdr	$⊢ (φ \land x \in B) \to x H x = x ({RingHom ↾}_{(B \times B)}) x$
31		eqid	$⊢ RingCat (U) = RingCat (U)$
32		eqid	$⊢ {Base}_{RingCat (U)} = {Base}_{RingCat (U)}$
33		eqid	$⊢ Hom (RingCat (U)) = Hom (RingCat (U))$
34	31 32 2 33	ringchomfval	$⊢ φ \to Hom (RingCat (U)) = {RingHom ↾}_{({Base}_{RingCat (U)} \times {Base}_{RingCat (U)})}$
35	31 32 2	ringcbas	$⊢ φ \to {Base}_{RingCat (U)} = U \cap Ring$
36		incom	$⊢ Ring \cap U = U \cap Ring$
37	3 36	eqtrdi	$⊢ φ \to B = U \cap Ring$
38	37	eqcomd	$⊢ φ \to U \cap Ring = B$
39	35 38	eqtrd	$⊢ φ \to {Base}_{RingCat (U)} = B$
40	39	sqxpeqd	$⊢ φ \to {Base}_{RingCat (U)} \times {Base}_{RingCat (U)} = B \times B$
41	40	reseq2d	$⊢ φ \to {RingHom ↾}_{({Base}_{RingCat (U)} \times {Base}_{RingCat (U)})} = {RingHom ↾}_{(B \times B)}$
42	34 41	eqtrd	$⊢ φ \to Hom (RingCat (U)) = {RingHom ↾}_{(B \times B)}$
43	42	adantr	$⊢ (φ \land x \in B) \to Hom (RingCat (U)) = {RingHom ↾}_{(B \times B)}$
44	43	eqcomd	$⊢ (φ \land x \in B) \to {RingHom ↾}_{(B \times B)} = Hom (RingCat (U))$
45	44	oveqd	$⊢ (φ \land x \in B) \to x ({RingHom ↾}_{(B \times B)}) x = x Hom (RingCat (U)) x$
46	37	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in (U \cap Ring))$
47	46	biimpa	$⊢ (φ \land x \in B) \to x \in (U \cap Ring)$
48	35	adantr	$⊢ (φ \land x \in B) \to {Base}_{RingCat (U)} = U \cap Ring$
49	47 48	eleqtrrd	$⊢ (φ \land x \in B) \to x \in {Base}_{RingCat (U)}$
50	31 32 15 33 49 49	ringchom	$⊢ (φ \land x \in B) \to x Hom (RingCat (U)) x = x RingHom x$
51	30 45 50	3eqtrd	$⊢ (φ \land x \in B) \to x H x = x RingHom x$
52	12 29 51	3eltr4d	$⊢ (φ \land x \in B) \to Id (C) (x) \in (x H x)$

Metamath Proof Explorer

Theorem rhmsubcrngclem1

Proof