funcringcsetcALTV2lem9

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

	Ref	Expression
Hypotheses	funcringcsetcALTV2.r	$⊢ R = RingCat (U)$
	funcringcsetcALTV2.s	$⊢ S = SetCat (U)$
	funcringcsetcALTV2.b	$⊢ B = {Base}_{R}$
	funcringcsetcALTV2.c	$⊢ C = {Base}_{S}$
	funcringcsetcALTV2.u	$⊢ φ \to U \in WUni$
	funcringcsetcALTV2.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
	funcringcsetcALTV2.g	$⊢ φ \to G = (x \in B, y \in B ⟼ {I ↾}_{(x RingHom y)})$
Assertion	funcringcsetcALTV2lem9	$⊢ (φ \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		funcringcsetcALTV2.r	$⊢ R = RingCat (U)$
2		funcringcsetcALTV2.s	$⊢ S = SetCat (U)$
3		funcringcsetcALTV2.b	$⊢ B = {Base}_{R}$
4		funcringcsetcALTV2.c	$⊢ C = {Base}_{S}$
5		funcringcsetcALTV2.u	$⊢ φ \to U \in WUni$
6		funcringcsetcALTV2.f	$⊢ φ \to F = (x \in B ⟼ {Base}_{x})$
7		funcringcsetcALTV2.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	ringchom	$⊢ (φ \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	ringchom	$⊢ (φ \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	funcringcsetcALTV2lem5	$⊢ (φ \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	1 3 5	ringcbas	$⊢ φ \to B = U \cap Ring$
29		inss1	$⊢ U \cap Ring \subseteq U$
30	28 29	eqsstrdi	$⊢ φ \to B \subseteq U$
31	30	sseld	$⊢ φ \to (X \in B \to X \in U)$
32	31	com12	$⊢ X \in B \to (φ \to X \in U)$
33	32	3ad2ant1	$⊢ (X \in B \land Y \in B \land Z \in B) \to (φ \to X \in U)$
34	33	impcom	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to X \in U$
35	34	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 U$
36	30	sseld	$⊢ φ \to (Y \in B \to Y \in U)$
37	36	com12	$⊢ Y \in B \to (φ \to Y \in U)$
38	37	3ad2ant2	$⊢ (X \in B \land Y \in B \land Z \in B) \to (φ \to Y \in U)$
39	38	impcom	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to Y \in U$
40	39	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 U$
41	30	sseld	$⊢ φ \to (Z \in B \to Z \in U)$
42	41	com12	$⊢ Z \in B \to (φ \to Z \in U)$
43	42	3ad2ant3	$⊢ (X \in B \land Y \in B \land Z \in B) \to (φ \to Z \in U)$
44	43	impcom	$⊢ (φ \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 (H \in (X RingHom Y) \land K \in (Y RingHom Z))) \to Z \in U$
46		eqid	$⊢ {Base}_{X} = {Base}_{X}$
47		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
48	46 47	rhmf	$⊢ H \in (X RingHom Y) \to H : {Base}_{X} ⟶ {Base}_{Y}$
49	48	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}$
50		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
51	47 50	rhmf	$⊢ K \in (Y RingHom Z) \to K : {Base}_{Y} ⟶ {Base}_{Z}$
52	51	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}$
53	1 26 27 35 40 45 49 52	ringcco	$⊢ ((φ \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$
54	25 53	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)$
55		eqid	$⊢ comp (S) = comp (S)$
56	1 2 3 4 5 6	funcringcsetcALTV2lem2	$⊢ (φ \land X \in B) \to F (X) \in U$
57	56	3ad2antr1	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (X) \in U$
58	57	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$
59	1 2 3 4 5 6	funcringcsetcALTV2lem2	$⊢ (φ \land Y \in B) \to F (Y) \in U$
60	59	3ad2antr2	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (Y) \in U$
61	60	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$
62	1 2 3 4 5 6	funcringcsetcALTV2lem2	$⊢ (φ \land Z \in B) \to F (Z) \in U$
63	62	3ad2antr3	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (Z) \in U$
64	63	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$
65	1 2 3 4 5 6	funcringcsetcALTV2lem1	$⊢ (φ \land X \in B) \to F (X) = {Base}_{X}$
66	65	3ad2antr1	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (X) = {Base}_{X}$
67	1 2 3 4 5 6	funcringcsetcALTV2lem1	$⊢ (φ \land Y \in B) \to F (Y) = {Base}_{Y}$
68	67	3ad2antr2	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (Y) = {Base}_{Y}$
69	66 68	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})$
70	69	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})$
71	49 70	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)$
72		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 φ$
73		3simpa	$⊢ (X \in B \land Y \in B \land Z \in B) \to (X \in B \land Y \in B)$
74	73	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)$
75		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)$
76	1 2 3 4 5 6 7	funcringcsetcALTV2lem6	$⊢ (φ \land (X \in B \land Y \in B) \land H \in (X RingHom Y)) \to (X G Y) (H) = H$
77	72 74 75 76	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$
78	77	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))$
79	71 78	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)$
80	1 2 3 4 5 6	funcringcsetcALTV2lem1	$⊢ (φ \land Z \in B) \to F (Z) = {Base}_{Z}$
81	80	3ad2antr3	$⊢ (φ \land (X \in B \land Y \in B \land Z \in B)) \to F (Z) = {Base}_{Z}$
82	68 81	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})$
83	82	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})$
84	52 83	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)$
85		3simpc	$⊢ (X \in B \land Y \in B \land Z \in B) \to (Y \in B \land Z \in B)$
86	85	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)$
87		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)$
88	1 2 3 4 5 6 7	funcringcsetcALTV2lem6	$⊢ (φ \land (Y \in B \land Z \in B) \land K \in (Y RingHom Z)) \to (Y G Z) (K) = K$
89	72 86 87 88	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$
90	89	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))$
91	84 90	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)$
92	2 26 55 58 61 64 79 91	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)$
93	89 77	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$
94	92 93	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$
95	22 54 94	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)$
96	95	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))$
97	17 96	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))$
98	97	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 funcringcsetcALTV2lem9

Proof