rhmsubcsetclem2

	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	rhmsubcsetclem2	$⊢ (φ \land x \in B) \to \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ comp (C) z) f \in (x H z)$

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		simpl	$⊢ (φ \land x \in B) \to φ$
6	5	adantr	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to φ$
7	6	adantr	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to φ$
8		simpr	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to (y \in B \land z \in B)$
9	8	adantr	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to (y \in B \land z \in B)$
10		simpr	$⊢ (f \in (x H y) \land g \in (y H z)) \to g \in (y H z)$
11	10	adantl	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to g \in (y H z)$
12	4	rhmresel	$⊢ (φ \land (y \in B \land z \in B) \land g \in (y H z)) \to g \in (y RingHom z)$
13	7 9 11 12	syl3anc	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to g \in (y RingHom z)$
14		simpr	$⊢ (φ \land x \in B) \to x \in B$
15		simpl	$⊢ (y \in B \land z \in B) \to y \in B$
16	14 15	anim12i	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to (x \in B \land y \in B)$
17	16	adantr	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to (x \in B \land y \in B)$
18		simprl	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to f \in (x H y)$
19	4	rhmresel	$⊢ (φ \land (x \in B \land y \in B) \land f \in (x H y)) \to f \in (x RingHom y)$
20	7 17 18 19	syl3anc	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to f \in (x RingHom y)$
21		rhmco	$⊢ (g \in (y RingHom z) \land f \in (x RingHom y)) \to g \circ f \in (x RingHom z)$
22	13 20 21	syl2anc	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to g \circ f \in (x RingHom z)$
23	2	ad3antrrr	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to U \in V$
24		eqid	$⊢ comp (C) = comp (C)$
25	3	eleq2d	$⊢ φ \to (x \in B \leftrightarrow x \in (Ring \cap U))$
26		elinel2	$⊢ x \in (Ring \cap U) \to x \in U$
27	25 26	syl6bi	$⊢ φ \to (x \in B \to x \in U)$
28	27	imp	$⊢ (φ \land x \in B) \to x \in U$
29	28	adantr	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to x \in U$
30	29	adantr	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to x \in U$
31	3	eleq2d	$⊢ φ \to (y \in B \leftrightarrow y \in (Ring \cap U))$
32		elinel2	$⊢ y \in (Ring \cap U) \to y \in U$
33	31 32	syl6bi	$⊢ φ \to (y \in B \to y \in U)$
34	33	adantr	$⊢ (φ \land x \in B) \to (y \in B \to y \in U)$
35	34	com12	$⊢ y \in B \to ((φ \land x \in B) \to y \in U)$
36	35	adantr	$⊢ (y \in B \land z \in B) \to ((φ \land x \in B) \to y \in U)$
37	36	impcom	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to y \in U$
38	37	adantr	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to y \in U$
39	3	eleq2d	$⊢ φ \to (z \in B \leftrightarrow z \in (Ring \cap U))$
40		elinel2	$⊢ z \in (Ring \cap U) \to z \in U$
41	39 40	syl6bi	$⊢ φ \to (z \in B \to z \in U)$
42	41	adantr	$⊢ (φ \land x \in B) \to (z \in B \to z \in U)$
43	42	adantld	$⊢ (φ \land x \in B) \to ((y \in B \land z \in B) \to z \in U)$
44	43	imp	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to z \in U$
45	44	adantr	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to z \in U$
46		eqid	$⊢ {Base}_{x} = {Base}_{x}$
47		eqid	$⊢ {Base}_{y} = {Base}_{y}$
48		eqid	$⊢ {Base}_{z} = {Base}_{z}$
49		simprl	$⊢ (y \in B \land (φ \land x \in B)) \to φ$
50	49	adantr	$⊢ ((y \in B \land (φ \land x \in B)) \land f \in (x H y)) \to φ$
51	14	anim1i	$⊢ ((φ \land x \in B) \land y \in B) \to (x \in B \land y \in B)$
52	51	ancoms	$⊢ (y \in B \land (φ \land x \in B)) \to (x \in B \land y \in B)$
53	52	adantr	$⊢ ((y \in B \land (φ \land x \in B)) \land f \in (x H y)) \to (x \in B \land y \in B)$
54		simpr	$⊢ ((y \in B \land (φ \land x \in B)) \land f \in (x H y)) \to f \in (x H y)$
55	50 53 54 19	syl3anc	$⊢ ((y \in B \land (φ \land x \in B)) \land f \in (x H y)) \to f \in (x RingHom y)$
56	46 47	rhmf	$⊢ f \in (x RingHom y) \to f : {Base}_{x} ⟶ {Base}_{y}$
57	55 56	syl	$⊢ ((y \in B \land (φ \land x \in B)) \land f \in (x H y)) \to f : {Base}_{x} ⟶ {Base}_{y}$
58	57	ex	$⊢ (y \in B \land (φ \land x \in B)) \to (f \in (x H y) \to f : {Base}_{x} ⟶ {Base}_{y})$
59	58	ex	$⊢ y \in B \to ((φ \land x \in B) \to (f \in (x H y) \to f : {Base}_{x} ⟶ {Base}_{y}))$
60	59	adantr	$⊢ (y \in B \land z \in B) \to ((φ \land x \in B) \to (f \in (x H y) \to f : {Base}_{x} ⟶ {Base}_{y}))$
61	60	impcom	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to (f \in (x H y) \to f : {Base}_{x} ⟶ {Base}_{y})$
62	61	com12	$⊢ f \in (x H y) \to (((φ \land x \in B) \land (y \in B \land z \in B)) \to f : {Base}_{x} ⟶ {Base}_{y})$
63	62	adantr	$⊢ (f \in (x H y) \land g \in (y H z)) \to (((φ \land x \in B) \land (y \in B \land z \in B)) \to f : {Base}_{x} ⟶ {Base}_{y})$
64	63	impcom	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to f : {Base}_{x} ⟶ {Base}_{y}$
65	12	3expa	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y H z)) \to g \in (y RingHom z)$
66	47 48	rhmf	$⊢ g \in (y RingHom z) \to g : {Base}_{y} ⟶ {Base}_{z}$
67	65 66	syl	$⊢ ((φ \land (y \in B \land z \in B)) \land g \in (y H z)) \to g : {Base}_{y} ⟶ {Base}_{z}$
68	67	ex	$⊢ (φ \land (y \in B \land z \in B)) \to (g \in (y H z) \to g : {Base}_{y} ⟶ {Base}_{z})$
69	68	adantlr	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to (g \in (y H z) \to g : {Base}_{y} ⟶ {Base}_{z})$
70	69	adantld	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to ((f \in (x H y) \land g \in (y H z)) \to g : {Base}_{y} ⟶ {Base}_{z})$
71	70	imp	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to g : {Base}_{y} ⟶ {Base}_{z}$
72	1 23 24 30 38 45 46 47 48 64 71	estrcco	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to g (⟨x, y⟩ comp (C) z) f = g \circ f$
73	4	adantr	$⊢ (φ \land x \in B) \to H = {RingHom ↾}_{(B \times B)}$
74	73	oveqdr	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to x H z = x ({RingHom ↾}_{(B \times B)}) z$
75		ovres	$⊢ (x \in B \land z \in B) \to x ({RingHom ↾}_{(B \times B)}) z = x RingHom z$
76	75	ad2ant2l	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to x ({RingHom ↾}_{(B \times B)}) z = x RingHom z$
77	74 76	eqtrd	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to x H z = x RingHom z$
78	77	adantr	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to x H z = x RingHom z$
79	22 72 78	3eltr4d	$⊢ (((φ \land x \in B) \land (y \in B \land z \in B)) \land (f \in (x H y) \land g \in (y H z))) \to g (⟨x, y⟩ comp (C) z) f \in (x H z)$
80	79	ralrimivva	$⊢ ((φ \land x \in B) \land (y \in B \land z \in B)) \to \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ comp (C) z) f \in (x H z)$
81	80	ralrimivva	$⊢ (φ \land x \in B) \to \forall y \in B \forall z \in B \forall f \in (x H y) \forall g \in (y H z) g (⟨x, y⟩ comp (C) z) f \in (x H z)$

Metamath Proof Explorer

Theorem rhmsubcsetclem2

Proof