funcringcsetclem9ALTV

Description: Lemma 9 for funcringcsetcALTV . (Contributed by AV, 15-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	funcringcsetcALTV.r	$⊢ R = RingCatALTV (U)$
	funcringcsetcALTV.s	$⊢ S = SetCat (U)$
	funcringcsetcALTV.b	$⊢ B = {Base}_{R}$
	funcringcsetcALTV.c	$⊢ C = {Base}_{S}$
	funcringcsetcALTV.u	$⊢ φ \to U \in WUni$
	funcringcsetcALTV.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
	funcringcsetcALTV.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RingHom y)})$
Assertion	funcringcsetclem9ALTV	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B) \land (H \in (X Hom (R) Y) \land K \in (Y Hom (R) Z))) \to (X G Z) (K (⟨X, Y⟩ comp (R) Z) H) = (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H)$

Proof

Step	Hyp	Ref	Expression
1		funcringcsetcALTV.r	$⊢ R = RingCatALTV (U)$
2		funcringcsetcALTV.s	$⊢ S = SetCat (U)$
3		funcringcsetcALTV.b	$⊢ B = {Base}_{R}$
4		funcringcsetcALTV.c	$⊢ C = {Base}_{S}$
5		funcringcsetcALTV.u	$⊢ φ \to U \in WUni$
6		funcringcsetcALTV.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
7		funcringcsetcALTV.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RingHom y)})$
8	5	adantr	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to U \in WUni$
9		eqid	$⊢ Hom (R) = Hom (R)$
10		simpr1	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to X \in B$
11		simpr2	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to Y \in B$
12	1 3 8 9 10 11	ringchomALTV	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to X Hom (R) Y = X RingHom Y$
13	12	eleq2d	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to (H \in (X Hom (R) Y) \leftrightarrow H \in (X RingHom Y))$
14		simpr3	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to Z \in B$
15	1 3 8 9 11 14	ringchomALTV	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to Y Hom (R) Z = Y RingHom Z$
16	15	eleq2d	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to (K \in (Y Hom (R) Z) \leftrightarrow K \in (Y RingHom Z))$
17	13 16	anbi12d	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to ((H \in (X Hom (R) Y) \land K \in (Y Hom (R) Z)) \leftrightarrow (H \in (X RingHom Y) \land K \in (Y RingHom Z)))$
18		rhmco	$⊢ (K \in (Y RingHom Z) \land H \in (X RingHom Y)) \to K \circ H \in (X RingHom Z)$
19	18	ancoms	$⊢ (H \in (X RingHom Y) \land K \in (Y RingHom Z)) \to K \circ H \in (X RingHom Z)$
20	19	adantl	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to K \circ H \in (X RingHom Z)$
21		fvresi	$⊢ K \circ H \in (X RingHom Z) \to ({I ↾}_{(X RingHom Z)}) (K \circ H) = K \circ H$
22	20 21	syl	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to ({I ↾}_{(X RingHom Z)}) (K \circ H) = K \circ H$
23	1 2 3 4 5 6 7	funcringcsetclem5ALTV	$⊢ (φ \land (X \in B \land Z \in B)) \to X G Z = {I ↾}_{(X RingHom Z)}$
24	23	3adantr2	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to X G Z = {I ↾}_{(X RingHom Z)}$
25	24	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to X G Z = {I ↾}_{(X RingHom Z)}$
26	8	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to U \in WUni$
27		eqid	$⊢ comp (R) = comp (R)$
28	10	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to X \in B$
29	11	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to Y \in B$
30	14	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to Z \in B$
31		simprl	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to H \in (X RingHom Y)$
32		simprr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to K \in (Y RingHom Z)$
33	1 3 26 27 28 29 30 31 32	ringccoALTV	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to K (⟨X, Y⟩ comp (R) Z) H = K \circ H$
34	25 33	fveq12d	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (X G Z) (K (⟨X, Y⟩ comp (R) Z) H) = ({I ↾}_{(X RingHom Z)}) (K \circ H)$
35		eqid	$⊢ comp (S) = comp (S)$
36	1 2 3 4 5 6	funcringcsetclem2ALTV	$⊢ (φ \land X \in B) \to F (X) \in U$
37	36	3ad2antr1	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (X) \in U$
38	37	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to F (X) \in U$
39	1 2 3 4 5 6	funcringcsetclem2ALTV	$⊢ (φ \land Y \in B) \to F (Y) \in U$
40	39	3ad2antr2	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (Y) \in U$
41	40	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to F (Y) \in U$
42	1 2 3 4 5 6	funcringcsetclem2ALTV	$⊢ (φ \land Z \in B) \to F (Z) \in U$
43	42	3ad2antr3	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (Z) \in U$
44	43	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to F (Z) \in U$
45		eqid	$⊢ {Base}_{X} = {Base}_{X}$
46		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
47	45 46	rhmf	$⊢ H \in (X RingHom Y) \to H : {Base}_{X} ⟶ {Base}_{Y}$
48	47	ad2antrl	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to H : {Base}_{X} ⟶ {Base}_{Y}$
49	1 2 3 4 5 6	funcringcsetclem1ALTV	$⊢ (φ \land X \in B) \to F (X) = {Base}_{X}$
50	49	3ad2antr1	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (X) = {Base}_{X}$
51	1 2 3 4 5 6	funcringcsetclem1ALTV	$⊢ (φ \land Y \in B) \to F (Y) = {Base}_{Y}$
52	51	3ad2antr2	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (Y) = {Base}_{Y}$
53	50 52	feq23d	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to (H : F (X) ⟶ F (Y) \leftrightarrow H : {Base}_{X} ⟶ {Base}_{Y})$
54	53	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (H : F (X) ⟶ F (Y) \leftrightarrow H : {Base}_{X} ⟶ {Base}_{Y})$
55	48 54	mpbird	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to H : F (X) ⟶ F (Y)$
56		simpll	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to φ$
57		3simpa	$⊢ (X \in B \land Y \in B \land Z \in B) \to (X \in B \land Y \in B)$
58	57	ad2antlr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (X \in B \land Y \in B)$
59	1 2 3 4 5 6 7	funcringcsetclem6ALTV	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (X RingHom Y)) \to (X G Y) (H) = H$
60	56 58 31 59	syl3anc	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (X G Y) (H) = H$
61	60	feq1d	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to ((X G Y) (H) : F (X) ⟶ F (Y) \leftrightarrow H : F (X) ⟶ F (Y))$
62	55 61	mpbird	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (X G Y) (H) : F (X) ⟶ F (Y)$
63		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
64	46 63	rhmf	$⊢ K \in (Y RingHom Z) \to K : {Base}_{Y} ⟶ {Base}_{Z}$
65	64	ad2antll	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to K : {Base}_{Y} ⟶ {Base}_{Z}$
66	1 2 3 4 5 6	funcringcsetclem1ALTV	$⊢ (φ \land Z \in B) \to F (Z) = {Base}_{Z}$
67	66	3ad2antr3	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (Z) = {Base}_{Z}$
68	52 67	feq23d	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to (K : F (Y) ⟶ F (Z) \leftrightarrow K : {Base}_{Y} ⟶ {Base}_{Z})$
69	68	adantr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (K : F (Y) ⟶ F (Z) \leftrightarrow K : {Base}_{Y} ⟶ {Base}_{Z})$
70	65 69	mpbird	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to K : F (Y) ⟶ F (Z)$
71		3simpc	$⊢ (X \in B \land Y \in B \land Z \in B) \to (Y \in B \land Z \in B)$
72	71	ad2antlr	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (Y \in B \land Z \in B)$
73	1 2 3 4 5 6 7	funcringcsetclem6ALTV	$⊢ (φ \land (Y \in B \land Z \in B) \land K \in (Y RingHom Z)) \to (Y G Z) (K) = K$
74	56 72 32 73	syl3anc	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (Y G Z) (K) = K$
75	74	feq1d	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to ((Y G Z) (K) : F (Y) ⟶ F (Z) \leftrightarrow K : F (Y) ⟶ F (Z))$
76	70 75	mpbird	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (Y G Z) (K) : F (Y) ⟶ F (Z)$
77	2 26 35 38 41 44 62 76	setcco	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H) = (Y G Z) (K) \circ (X G Y) (H)$
78	74 60	coeq12d	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (Y G Z) (K) \circ (X G Y) (H) = K \circ H$
79	77 78	eqtrd	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H) = K \circ H$
80	22 34 79	3eqtr4d	$⊢ ((φ \land (X \in B \land Y \in B \land Z \in B)) \land (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to (X G Z) (K (⟨X, Y⟩ comp (R) Z) H) = (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H)$
81	80	ex	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to ((H \in (X RingHom Y) \land K \in (Y RingHom Z)) \to (X G Z) (K (⟨X, Y⟩ comp (R) Z) H) = (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H))$
82	17 81	sylbid	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to ((H \in (X Hom (R) Y) \land K \in (Y Hom (R) Z)) \to (X G Z) (K (⟨X, Y⟩ comp (R) Z) H) = (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H))$
83	82	3impia	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B) \land (H \in (X Hom (R) Y) \land K \in (Y Hom (R) Z))) \to (X G Z) (K (⟨X, Y⟩ comp (R) Z) H) = (Y G Z) (K) (⟨F (X), F (Y)⟩ comp (S) F (Z)) (X G Y) (H)$

Metamath Proof Explorer

Theorem funcringcsetclem9ALTV

Proof