ringccatidALTV

Description: Lemma for ringccatALTV . (Contributed by AV, 14-Feb-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ringccatALTV.c	$⊢ C = RingCatALTV (U)$
	ringccatidALTV.b	$⊢ B = {Base}_{C}$
Assertion	ringccatidALTV	$⊢ U \in V \to (C \in Cat \land Id (C) = (x \in B ⟼ {I ↾}_{{Base}_{x}}))$

Proof

Step	Hyp	Ref	Expression
1		ringccatALTV.c	$⊢ C = RingCatALTV (U)$
2		ringccatidALTV.b	$⊢ B = {Base}_{C}$
3	2	a1i	$⊢ U \in V \to B = {Base}_{C}$
4		eqidd	$⊢ U \in V \to Hom (C) = Hom (C)$
5		eqidd	$⊢ U \in V \to comp (C) = comp (C)$
6	1	fvexi	$⊢ C \in V$
7	6	a1i	$⊢ U \in V \to C \in V$
8		biid	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \leftrightarrow ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))$
9		simpl	$⊢ (U \in V \land x \in B) \to U \in V$
10	1 2 9	ringcbasALTV	$⊢ (U \in V \land x \in B) \to B = U \cap Ring$
11		eleq2	$⊢ B = U \cap Ring \to (x \in B \leftrightarrow x \in (U \cap Ring))$
12		elin	$⊢ x \in (U \cap Ring) \leftrightarrow (x \in U \land x \in Ring)$
13	12	simprbi	$⊢ x \in (U \cap Ring) \to x \in Ring$
14	11 13	biimtrdi	$⊢ B = U \cap Ring \to (x \in B \to x \in Ring)$
15	14	com12	$⊢ x \in B \to (B = U \cap Ring \to x \in Ring)$
16	15	adantl	$⊢ (U \in V \land x \in B) \to (B = U \cap Ring \to x \in Ring)$
17	10 16	mpd	$⊢ (U \in V \land x \in B) \to x \in Ring$
18		eqid	$⊢ {Base}_{x} = {Base}_{x}$
19	18	idrhm	$⊢ x \in Ring \to {I ↾}_{{Base}_{x}} \in (x RingHom x)$
20	17 19	syl	$⊢ (U \in V \land x \in B) \to {I ↾}_{{Base}_{x}} \in (x RingHom x)$
21		eqid	$⊢ Hom (C) = Hom (C)$
22		simpr	$⊢ (U \in V \land x \in B) \to x \in B$
23	1 2 9 21 22 22	ringchomALTV	$⊢ (U \in V \land x \in B) \to x Hom (C) x = x RingHom x$
24	20 23	eleqtrrd	$⊢ (U \in V \land x \in B) \to {I ↾}_{{Base}_{x}} \in (x Hom (C) x)$
25		simpl	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to U \in V$
26		eqid	$⊢ comp (C) = comp (C)$
27		simpl	$⊢ (w \in B \land x \in B) \to w \in B$
28	27	3ad2ant1	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \to w \in B$
29	28	adantl	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to w \in B$
30		simpr	$⊢ (w \in B \land x \in B) \to x \in B$
31	30	3ad2ant1	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \to x \in B$
32	31	adantl	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to x \in B$
33		simp1	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to U \in V$
34	27	3ad2ant3	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to w \in B$
35	30	3ad2ant3	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to x \in B$
36	1 2 33 21 34 35	ringchomALTV	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to w Hom (C) x = w RingHom x$
37	36	eleq2d	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to (f \in (w Hom (C) x) \leftrightarrow f \in (w RingHom x))$
38	37	biimpd	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to (f \in (w Hom (C) x) \to f \in (w RingHom x))$
39	38	3exp	$⊢ U \in V \to ((y \in B \land z \in B) \to ((w \in B \land x \in B) \to (f \in (w Hom (C) x) \to f \in (w RingHom x))))$
40	39	com14	$⊢ f \in (w Hom (C) x) \to ((y \in B \land z \in B) \to ((w \in B \land x \in B) \to (U \in V \to f \in (w RingHom x))))$
41	40	3ad2ant1	$⊢ (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)) \to ((y \in B \land z \in B) \to ((w \in B \land x \in B) \to (U \in V \to f \in (w RingHom x))))$
42	41	com13	$⊢ (w \in B \land x \in B) \to ((y \in B \land z \in B) \to ((f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)) \to (U \in V \to f \in (w RingHom x))))$
43	42	3imp	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \to (U \in V \to f \in (w RingHom x))$
44	43	impcom	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to f \in (w RingHom x)$
45	20	expcom	$⊢ x \in B \to (U \in V \to {I ↾}_{{Base}_{x}} \in (x RingHom x))$
46	45	adantl	$⊢ (w \in B \land x \in B) \to (U \in V \to {I ↾}_{{Base}_{x}} \in (x RingHom x))$
47	46	3ad2ant1	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \to (U \in V \to {I ↾}_{{Base}_{x}} \in (x RingHom x))$
48	47	impcom	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to {I ↾}_{{Base}_{x}} \in (x RingHom x)$
49	1 2 25 26 29 32 32 44 48	ringccoALTV	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to ({I ↾}_{{Base}_{x}}) (⟨w, x⟩ comp (C) x) f = ({I ↾}_{{Base}_{x}}) \circ f$
50		simpl	$⊢ (U \in V \land (w \in B \land x \in B)) \to U \in V$
51		simprl	$⊢ (U \in V \land (w \in B \land x \in B)) \to w \in B$
52		simprr	$⊢ (U \in V \land (w \in B \land x \in B)) \to x \in B$
53	1 2 50 21 51 52	elringchomALTV	$⊢ (U \in V \land (w \in B \land x \in B)) \to (f \in (w Hom (C) x) \to f : {Base}_{w} ⟶ {Base}_{x})$
54	53	ex	$⊢ U \in V \to ((w \in B \land x \in B) \to (f \in (w Hom (C) x) \to f : {Base}_{w} ⟶ {Base}_{x}))$
55	54	com13	$⊢ f \in (w Hom (C) x) \to ((w \in B \land x \in B) \to (U \in V \to f : {Base}_{w} ⟶ {Base}_{x}))$
56		fcoi2	$⊢ f : {Base}_{w} ⟶ {Base}_{x} \to ({I ↾}_{{Base}_{x}}) \circ f = f$
57	55 56	syl8	$⊢ f \in (w Hom (C) x) \to ((w \in B \land x \in B) \to (U \in V \to ({I ↾}_{{Base}_{x}}) \circ f = f))$
58	57	3ad2ant1	$⊢ (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)) \to ((w \in B \land x \in B) \to (U \in V \to ({I ↾}_{{Base}_{x}}) \circ f = f))$
59	58	com12	$⊢ (w \in B \land x \in B) \to ((f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)) \to (U \in V \to ({I ↾}_{{Base}_{x}}) \circ f = f))$
60	59	a1d	$⊢ (w \in B \land x \in B) \to ((y \in B \land z \in B) \to ((f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)) \to (U \in V \to ({I ↾}_{{Base}_{x}}) \circ f = f)))$
61	60	3imp	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \to (U \in V \to ({I ↾}_{{Base}_{x}}) \circ f = f)$
62	61	impcom	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to ({I ↾}_{{Base}_{x}}) \circ f = f$
63	49 62	eqtrd	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to ({I ↾}_{{Base}_{x}}) (⟨w, x⟩ comp (C) x) f = f$
64		simp3	$⊢ (g \in (x Hom (C) y) \land ((w \in B \land x \in B) \land (y \in B \land z \in B)) \land U \in V) \to U \in V$
65	30	adantr	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B)) \to x \in B$
66	65	3ad2ant2	$⊢ (g \in (x Hom (C) y) \land ((w \in B \land x \in B) \land (y \in B \land z \in B)) \land U \in V) \to x \in B$
67		simprl	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B)) \to y \in B$
68	67	3ad2ant2	$⊢ (g \in (x Hom (C) y) \land ((w \in B \land x \in B) \land (y \in B \land z \in B)) \land U \in V) \to y \in B$
69	46	adantr	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B)) \to (U \in V \to {I ↾}_{{Base}_{x}} \in (x RingHom x))$
70	69	a1i	$⊢ g \in (x Hom (C) y) \to (((w \in B \land x \in B) \land (y \in B \land z \in B)) \to (U \in V \to {I ↾}_{{Base}_{x}} \in (x RingHom x)))$
71	70	3imp	$⊢ (g \in (x Hom (C) y) \land ((w \in B \land x \in B) \land (y \in B \land z \in B)) \land U \in V) \to {I ↾}_{{Base}_{x}} \in (x RingHom x)$
72		simpl	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B))) \to U \in V$
73	65	adantl	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B))) \to x \in B$
74	67	adantl	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B))) \to y \in B$
75	1 2 72 21 73 74	ringchomALTV	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B))) \to x Hom (C) y = x RingHom y$
76	75	eleq2d	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B))) \to (g \in (x Hom (C) y) \leftrightarrow g \in (x RingHom y))$
77	76	biimpd	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B))) \to (g \in (x Hom (C) y) \to g \in (x RingHom y))$
78	77	ex	$⊢ U \in V \to (((w \in B \land x \in B) \land (y \in B \land z \in B)) \to (g \in (x Hom (C) y) \to g \in (x RingHom y)))$
79	78	com13	$⊢ g \in (x Hom (C) y) \to (((w \in B \land x \in B) \land (y \in B \land z \in B)) \to (U \in V \to g \in (x RingHom y)))$
80	79	3imp	$⊢ (g \in (x Hom (C) y) \land ((w \in B \land x \in B) \land (y \in B \land z \in B)) \land U \in V) \to g \in (x RingHom y)$
81	1 2 64 26 66 66 68 71 80	ringccoALTV	$⊢ (g \in (x Hom (C) y) \land ((w \in B \land x \in B) \land (y \in B \land z \in B)) \land U \in V) \to g (⟨x, x⟩ comp (C) y) ({I ↾}_{{Base}_{x}}) = g \circ ({I ↾}_{{Base}_{x}})$
82	1 2 72 21 73 74	elringchomALTV	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B))) \to (g \in (x Hom (C) y) \to g : {Base}_{x} ⟶ {Base}_{y})$
83	82	ex	$⊢ U \in V \to (((w \in B \land x \in B) \land (y \in B \land z \in B)) \to (g \in (x Hom (C) y) \to g : {Base}_{x} ⟶ {Base}_{y}))$
84	83	com13	$⊢ g \in (x Hom (C) y) \to (((w \in B \land x \in B) \land (y \in B \land z \in B)) \to (U \in V \to g : {Base}_{x} ⟶ {Base}_{y}))$
85	84	3imp	$⊢ (g \in (x Hom (C) y) \land ((w \in B \land x \in B) \land (y \in B \land z \in B)) \land U \in V) \to g : {Base}_{x} ⟶ {Base}_{y}$
86		fcoi1	$⊢ g : {Base}_{x} ⟶ {Base}_{y} \to g \circ ({I ↾}_{{Base}_{x}}) = g$
87	85 86	syl	$⊢ (g \in (x Hom (C) y) \land ((w \in B \land x \in B) \land (y \in B \land z \in B)) \land U \in V) \to g \circ ({I ↾}_{{Base}_{x}}) = g$
88	81 87	eqtrd	$⊢ (g \in (x Hom (C) y) \land ((w \in B \land x \in B) \land (y \in B \land z \in B)) \land U \in V) \to g (⟨x, x⟩ comp (C) y) ({I ↾}_{{Base}_{x}}) = g$
89	88	3exp	$⊢ g \in (x Hom (C) y) \to (((w \in B \land x \in B) \land (y \in B \land z \in B)) \to (U \in V \to g (⟨x, x⟩ comp (C) y) ({I ↾}_{{Base}_{x}}) = g))$
90	89	3ad2ant2	$⊢ (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)) \to (((w \in B \land x \in B) \land (y \in B \land z \in B)) \to (U \in V \to g (⟨x, x⟩ comp (C) y) ({I ↾}_{{Base}_{x}}) = g))$
91	90	expdcom	$⊢ (w \in B \land x \in B) \to ((y \in B \land z \in B) \to ((f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)) \to (U \in V \to g (⟨x, x⟩ comp (C) y) ({I ↾}_{{Base}_{x}}) = g)))$
92	91	3imp	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \to (U \in V \to g (⟨x, x⟩ comp (C) y) ({I ↾}_{{Base}_{x}}) = g)$
93	92	impcom	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g (⟨x, x⟩ comp (C) y) ({I ↾}_{{Base}_{x}}) = g$
94		simpl	$⊢ (y \in B \land z \in B) \to y \in B$
95	94	3ad2ant2	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to y \in B$
96	1 2 33 21 35 95	ringchomALTV	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to x Hom (C) y = x RingHom y$
97	96	eleq2d	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to (g \in (x Hom (C) y) \leftrightarrow g \in (x RingHom y))$
98	97	biimpd	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to (g \in (x Hom (C) y) \to g \in (x RingHom y))$
99	98	3exp	$⊢ U \in V \to ((y \in B \land z \in B) \to ((w \in B \land x \in B) \to (g \in (x Hom (C) y) \to g \in (x RingHom y))))$
100	99	com14	$⊢ g \in (x Hom (C) y) \to ((y \in B \land z \in B) \to ((w \in B \land x \in B) \to (U \in V \to g \in (x RingHom y))))$
101	100	3ad2ant2	$⊢ (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)) \to ((y \in B \land z \in B) \to ((w \in B \land x \in B) \to (U \in V \to g \in (x RingHom y))))$
102	101	com13	$⊢ (w \in B \land x \in B) \to ((y \in B \land z \in B) \to ((f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)) \to (U \in V \to g \in (x RingHom y))))$
103	102	3imp	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \to (U \in V \to g \in (x RingHom y))$
104	103	impcom	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g \in (x RingHom y)$
105		rhmco	$⊢ (g \in (x RingHom y) \land f \in (w RingHom x)) \to g \circ f \in (w RingHom y)$
106	104 44 105	syl2anc	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g \circ f \in (w RingHom y)$
107	94	3ad2ant2	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \to y \in B$
108	107	adantl	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to y \in B$
109	1 2 25 26 29 32 108 44 104	ringccoALTV	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g (⟨w, x⟩ comp (C) y) f = g \circ f$
110	1 2 25 21 29 108	ringchomALTV	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to w Hom (C) y = w RingHom y$
111	106 109 110	3eltr4d	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to g (⟨w, x⟩ comp (C) y) f \in (w Hom (C) y)$
112		coass	$⊢ (h \circ g) \circ f = h \circ (g \circ f)$
113		simp2r	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \to z \in B$
114	113	adantl	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to z \in B$
115		simp2r	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to z \in B$
116	1 2 33 21 95 115	ringchomALTV	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to y Hom (C) z = y RingHom z$
117	116	eleq2d	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to (h \in (y Hom (C) z) \leftrightarrow h \in (y RingHom z))$
118	117	biimpd	$⊢ (U \in V \land (y \in B \land z \in B) \land (w \in B \land x \in B)) \to (h \in (y Hom (C) z) \to h \in (y RingHom z))$
119	118	3exp	$⊢ U \in V \to ((y \in B \land z \in B) \to ((w \in B \land x \in B) \to (h \in (y Hom (C) z) \to h \in (y RingHom z))))$
120	119	com14	$⊢ h \in (y Hom (C) z) \to ((y \in B \land z \in B) \to ((w \in B \land x \in B) \to (U \in V \to h \in (y RingHom z))))$
121	120	3ad2ant3	$⊢ (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)) \to ((y \in B \land z \in B) \to ((w \in B \land x \in B) \to (U \in V \to h \in (y RingHom z))))$
122	121	com13	$⊢ (w \in B \land x \in B) \to ((y \in B \land z \in B) \to ((f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)) \to (U \in V \to h \in (y RingHom z))))$
123	122	3imp	$⊢ ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z))) \to (U \in V \to h \in (y RingHom z))$
124	123	impcom	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to h \in (y RingHom z)$
125		rhmco	$⊢ (h \in (y RingHom z) \land g \in (x RingHom y)) \to h \circ g \in (x RingHom z)$
126	124 104 125	syl2anc	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to h \circ g \in (x RingHom z)$
127	1 2 25 26 29 32 114 44 126	ringccoALTV	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (h \circ g) (⟨w, x⟩ comp (C) z) f = (h \circ g) \circ f$
128	1 2 25 26 29 108 114 106 124	ringccoALTV	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to h (⟨w, y⟩ comp (C) z) (g \circ f) = h \circ (g \circ f)$
129	112 127 128	3eqtr4a	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (h \circ g) (⟨w, x⟩ comp (C) z) f = h (⟨w, y⟩ comp (C) z) (g \circ f)$
130	1 2 25 26 32 108 114 104 124	ringccoALTV	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to h (⟨x, y⟩ comp (C) z) g = h \circ g$
131	130	oveq1d	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (h (⟨x, y⟩ comp (C) z) g) (⟨w, x⟩ comp (C) z) f = (h \circ g) (⟨w, x⟩ comp (C) z) f$
132	109	oveq2d	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to h (⟨w, y⟩ comp (C) z) (g (⟨w, x⟩ comp (C) y) f) = h (⟨w, y⟩ comp (C) z) (g \circ f)$
133	129 131 132	3eqtr4d	$⊢ (U \in V \land ((w \in B \land x \in B) \land (y \in B \land z \in B) \land (f \in (w Hom (C) x) \land g \in (x Hom (C) y) \land h \in (y Hom (C) z)))) \to (h (⟨x, y⟩ comp (C) z) g) (⟨w, x⟩ comp (C) z) f = h (⟨w, y⟩ comp (C) z) (g (⟨w, x⟩ comp (C) y) f)$
134	3 4 5 7 8 24 63 93 111 133	iscatd2	$⊢ U \in V \to (C \in Cat \land Id (C) = (x \in B ⟼ {I ↾}_{{Base}_{x}}))$

Metamath Proof Explorer

Theorem ringccatidALTV

Proof