rhmsubclem4

	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	rhmsubclem4	$⊢ (((φ \land x \in R) \land (y \in R \land z \in R)) \land (f \in (x H y) \land g \in (y H z))) \to g (⟨x, y⟩ comp (RngCat (U)) z) f \in (x H z)$

Proof

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		simpl	$⊢ (φ \land x \in R) \to φ$
6	5	adantr	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to φ$
7		simpr	$⊢ (φ \land x \in R) \to x \in R$
8	7	adantr	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to x \in R$
9		simpl	$⊢ (y \in R \land z \in R) \to y \in R$
10	9	adantl	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to y \in R$
11	1 2 3 4	rhmsubclem2	$⊢ (φ \land x \in R \land y \in R) \to x H y = x RingHom y$
12	6 8 10 11	syl3anc	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to x H y = x RingHom y$
13	12	eleq2d	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to (f \in (x H y) \leftrightarrow f \in (x RingHom y))$
14		simpr	$⊢ (y \in R \land z \in R) \to z \in R$
15	14	adantl	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to z \in R$
16	1 2 3 4	rhmsubclem2	$⊢ (φ \land y \in R \land z \in R) \to y H z = y RingHom z$
17	6 10 15 16	syl3anc	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to y H z = y RingHom z$
18	17	eleq2d	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to (g \in (y H z) \leftrightarrow g \in (y RingHom z))$
19	13 18	anbi12d	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to ((f \in (x H y) \land g \in (y H z)) \leftrightarrow (f \in (x RingHom y) \land g \in (y RingHom z)))$
20		rhmco	$⊢ (g \in (y RingHom z) \land f \in (x RingHom y)) \to g \circ f \in (x RingHom z)$
21	20	ancoms	$⊢ (f \in (x RingHom y) \land g \in (y RingHom z)) \to g \circ f \in (x RingHom z)$
22	19 21	syl6bi	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to ((f \in (x H y) \land g \in (y H z)) \to g \circ f \in (x RingHom z))$
23	22	imp	$⊢ (((φ \land x \in R) \land (y \in R \land z \in R)) \land (f \in (x H y) \land g \in (y H z))) \to g \circ f \in (x RingHom z)$
24	1	ad3antrrr	$⊢ (((φ \land x \in R) \land (y \in R \land z \in R)) \land (f \in (x H y) \land g \in (y H z))) \to U \in V$
25	2	eqcomi	$⊢ RngCat (U) = C$
26	25	fveq2i	$⊢ comp (RngCat (U)) = comp (C)$
27		inss2	$⊢ Ring \cap U \subseteq U$
28	3 27	eqsstrdi	$⊢ φ \to R \subseteq U$
29	28	sselda	$⊢ (φ \land x \in R) \to x \in U$
30	29	adantr	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to x \in U$
31	30	adantr	$⊢ (((φ \land x \in R) \land (y \in R \land z \in R)) \land (f \in (x H y) \land g \in (y H z))) \to x \in U$
32	28	sseld	$⊢ φ \to (y \in R \to y \in U)$
33	32	adantrd	$⊢ φ \to ((y \in R \land z \in R) \to y \in U)$
34	33	adantr	$⊢ (φ \land x \in R) \to ((y \in R \land z \in R) \to y \in U)$
35	34	imp	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to y \in U$
36	35	adantr	$⊢ (((φ \land x \in R) \land (y \in R \land z \in R)) \land (f \in (x H y) \land g \in (y H z))) \to y \in U$
37	28	sseld	$⊢ φ \to (z \in R \to z \in U)$
38	37	adantld	$⊢ φ \to ((y \in R \land z \in R) \to z \in U)$
39	38	adantr	$⊢ (φ \land x \in R) \to ((y \in R \land z \in R) \to z \in U)$
40	39	imp	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to z \in U$
41	40	adantr	$⊢ (((φ \land x \in R) \land (y \in R \land z \in R)) \land (f \in (x H y) \land g \in (y H z))) \to z \in U$
42	4	oveqi	$⊢ x H y = x ({RingHom ↾}_{(R \times R)}) y$
43	8 10	ovresd	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to x ({RingHom ↾}_{(R \times R)}) y = x RingHom y$
44	42 43	syl5eq	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to x H y = x RingHom y$
45	44	eleq2d	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to (f \in (x H y) \leftrightarrow f \in (x RingHom y))$
46		eqid	$⊢ {Base}_{x} = {Base}_{x}$
47		eqid	$⊢ {Base}_{y} = {Base}_{y}$
48	46 47	rhmf	$⊢ f \in (x RingHom y) \to f : {Base}_{x} ⟶ {Base}_{y}$
49	45 48	syl6bi	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to (f \in (x H y) \to f : {Base}_{x} ⟶ {Base}_{y})$
50	49	com12	$⊢ f \in (x H y) \to (((φ \land x \in R) \land (y \in R \land z \in R)) \to f : {Base}_{x} ⟶ {Base}_{y})$
51	50	adantr	$⊢ (f \in (x H y) \land g \in (y H z)) \to (((φ \land x \in R) \land (y \in R \land z \in R)) \to f : {Base}_{x} ⟶ {Base}_{y})$
52	51	impcom	$⊢ (((φ \land x \in R) \land (y \in R \land z \in R)) \land (f \in (x H y) \land g \in (y H z))) \to f : {Base}_{x} ⟶ {Base}_{y}$
53	4	oveqi	$⊢ y H z = y ({RingHom ↾}_{(R \times R)}) z$
54		ovres	$⊢ (y \in R \land z \in R) \to y ({RingHom ↾}_{(R \times R)}) z = y RingHom z$
55	54	adantl	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to y ({RingHom ↾}_{(R \times R)}) z = y RingHom z$
56	53 55	syl5eq	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to y H z = y RingHom z$
57	56	eleq2d	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to (g \in (y H z) \leftrightarrow g \in (y RingHom z))$
58		eqid	$⊢ {Base}_{z} = {Base}_{z}$
59	47 58	rhmf	$⊢ g \in (y RingHom z) \to g : {Base}_{y} ⟶ {Base}_{z}$
60	57 59	syl6bi	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to (g \in (y H z) \to g : {Base}_{y} ⟶ {Base}_{z})$
61	60	com12	$⊢ g \in (y H z) \to (((φ \land x \in R) \land (y \in R \land z \in R)) \to g : {Base}_{y} ⟶ {Base}_{z})$
62	61	adantl	$⊢ (f \in (x H y) \land g \in (y H z)) \to (((φ \land x \in R) \land (y \in R \land z \in R)) \to g : {Base}_{y} ⟶ {Base}_{z})$
63	62	impcom	$⊢ (((φ \land x \in R) \land (y \in R \land z \in R)) \land (f \in (x H y) \land g \in (y H z))) \to g : {Base}_{y} ⟶ {Base}_{z}$
64	2 24 26 31 36 41 52 63	rngcco	$⊢ (((φ \land x \in R) \land (y \in R \land z \in R)) \land (f \in (x H y) \land g \in (y H z))) \to g (⟨x, y⟩ comp (RngCat (U)) z) f = g \circ f$
65	1 2 3 4	rhmsubclem2	$⊢ (φ \land x \in R \land z \in R) \to x H z = x RingHom z$
66	6 8 15 65	syl3anc	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to x H z = x RingHom z$
67	66	adantr	$⊢ (((φ \land x \in R) \land (y \in R \land z \in R)) \land (f \in (x H y) \land g \in (y H z))) \to x H z = x RingHom z$
68	23 64 67	3eltr4d	$⊢ (((φ \land x \in R) \land (y \in R \land z \in R)) \land (f \in (x H y) \land g \in (y H z))) \to g (⟨x, y⟩ comp (RngCat (U)) z) f \in (x H z)$

Metamath Proof Explorer

Theorem rhmsubclem4

Proof