rhmsubcrngclem2

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

Proof