rhmsubcALTVlem4

Description: Lemma 4 for rhmsubcALTV . (Contributed by AV, 2-Mar-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	rngcrescrhmALTV.u	$⊢ φ \to U \in V$
	rngcrescrhmALTV.c	$⊢ C = RngCatALTV (U)$
	rngcrescrhmALTV.r	$⊢ φ \to R = Ring \cap U$
	rngcrescrhmALTV.h	$⊢ H = {RingHom ↾}_{(R \times R)}$
Assertion	rhmsubcALTVlem4	$⊢ (((φ \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 (RngCatALTV (U)) z) f \in (x H z)$

Proof

Step	Hyp	Ref	Expression
1		rngcrescrhmALTV.u	$⊢ φ \to U \in V$
2		rngcrescrhmALTV.c	$⊢ C = RngCatALTV (U)$
3		rngcrescrhmALTV.r	$⊢ φ \to R = Ring \cap U$
4		rngcrescrhmALTV.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	rhmsubcALTVlem2	$⊢ (φ \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	rhmsubcALTVlem2	$⊢ (φ \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		eqid	$⊢ RngCatALTV (U) = RngCatALTV (U)$
25		eqid	$⊢ {Base}_{RngCatALTV (U)} = {Base}_{RngCatALTV (U)}$
26	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$
27		eqid	$⊢ comp (RngCatALTV (U)) = comp (RngCatALTV (U))$
28		incom	$⊢ Ring \cap U = U \cap Ring$
29		ringrng	$⊢ x \in Ring \to x \in Rng$
30	29	a1i	$⊢ φ \to (x \in Ring \to x \in Rng)$
31	30	ssrdv	$⊢ φ \to Ring \subseteq Rng$
32		sslin	$⊢ Ring \subseteq Rng \to U \cap Ring \subseteq U \cap Rng$
33	31 32	syl	$⊢ φ \to U \cap Ring \subseteq U \cap Rng$
34	28 33	eqsstrid	$⊢ φ \to Ring \cap U \subseteq U \cap Rng$
35	24 25 1	rngcbasALTV	$⊢ φ \to {Base}_{RngCatALTV (U)} = U \cap Rng$
36	34 3 35	3sstr4d	$⊢ φ \to R \subseteq {Base}_{RngCatALTV (U)}$
37	36	sselda	$⊢ (φ \land x \in R) \to x \in {Base}_{RngCatALTV (U)}$
38	37	adantr	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to x \in {Base}_{RngCatALTV (U)}$
39	38	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 {Base}_{RngCatALTV (U)}$
40	36	sseld	$⊢ φ \to (y \in R \to y \in {Base}_{RngCatALTV (U)})$
41	40	adantr	$⊢ (φ \land x \in R) \to (y \in R \to y \in {Base}_{RngCatALTV (U)})$
42	41	com12	$⊢ y \in R \to ((φ \land x \in R) \to y \in {Base}_{RngCatALTV (U)})$
43	42	adantr	$⊢ (y \in R \land z \in R) \to ((φ \land x \in R) \to y \in {Base}_{RngCatALTV (U)})$
44	43	impcom	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to y \in {Base}_{RngCatALTV (U)}$
45	44	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 {Base}_{RngCatALTV (U)}$
46	36	sseld	$⊢ φ \to (z \in R \to z \in {Base}_{RngCatALTV (U)})$
47	46	adantr	$⊢ (φ \land x \in R) \to (z \in R \to z \in {Base}_{RngCatALTV (U)})$
48	47	adantld	$⊢ (φ \land x \in R) \to ((y \in R \land z \in R) \to z \in {Base}_{RngCatALTV (U)})$
49	48	imp	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to z \in {Base}_{RngCatALTV (U)}$
50	49	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 {Base}_{RngCatALTV (U)}$
51		rhmisrnghm	$⊢ f \in (x RingHom y) \to f \in (x RngHom y)$
52	13 51	syl6bi	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to (f \in (x H y) \to f \in (x RngHom y))$
53	52	com12	$⊢ f \in (x H y) \to (((φ \land x \in R) \land (y \in R \land z \in R)) \to f \in (x RngHom y))$
54	53	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 \in (x RngHom y))$
55	54	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 \in (x RngHom y)$
56		rhmisrnghm	$⊢ g \in (y RingHom z) \to g \in (y RngHom z)$
57	18 56	syl6bi	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to (g \in (y H z) \to g \in (y RngHom z))$
58	57	adantld	$⊢ ((φ \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 \in (y RngHom z))$
59	58	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 \in (y RngHom z)$
60	24 25 26 27 39 45 50 55 59	rngccoALTV	$⊢ (((φ \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 (RngCatALTV (U)) z) f = g \circ f$
61	1 2 3 4	rhmsubcALTVlem2	$⊢ (φ \land x \in R \land z \in R) \to x H z = x RingHom z$
62	6 8 15 61	syl3anc	$⊢ ((φ \land x \in R) \land (y \in R \land z \in R)) \to x H z = x RingHom z$
63	62	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$
64	23 60 63	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 (RngCatALTV (U)) z) f \in (x H z)$

Metamath Proof Explorer

Theorem rhmsubcALTVlem4

Proof