# Metamath Proof Explorer

## Theorem funcringcsetcALTV2lem9

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

Ref Expression
Hypotheses funcringcsetcALTV2.r ${⊢}{R}=\mathrm{RingCat}\left({U}\right)$
funcringcsetcALTV2.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
funcringcsetcALTV2.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
funcringcsetcALTV2.c ${⊢}{C}={\mathrm{Base}}_{{S}}$
funcringcsetcALTV2.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
funcringcsetcALTV2.f ${⊢}{\phi }\to {F}=\left({x}\in {B}⟼{\mathrm{Base}}_{{x}}\right)$
funcringcsetcALTV2.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({x}\mathrm{RingHom}{y}\right)}\right)$
Assertion funcringcsetcALTV2lem9 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\wedge \left({H}\in \left({X}\mathrm{Hom}\left({R}\right){Y}\right)\wedge {K}\in \left({Y}\mathrm{Hom}\left({R}\right){Z}\right)\right)\right)\to \left({X}{G}{Z}\right)\left({K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({R}\right){Z}\right){H}\right)=\left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)$

### Proof

Step Hyp Ref Expression
1 funcringcsetcALTV2.r ${⊢}{R}=\mathrm{RingCat}\left({U}\right)$
2 funcringcsetcALTV2.s ${⊢}{S}=\mathrm{SetCat}\left({U}\right)$
3 funcringcsetcALTV2.b ${⊢}{B}={\mathrm{Base}}_{{R}}$
4 funcringcsetcALTV2.c ${⊢}{C}={\mathrm{Base}}_{{S}}$
5 funcringcsetcALTV2.u ${⊢}{\phi }\to {U}\in \mathrm{WUni}$
6 funcringcsetcALTV2.f ${⊢}{\phi }\to {F}=\left({x}\in {B}⟼{\mathrm{Base}}_{{x}}\right)$
7 funcringcsetcALTV2.g ${⊢}{\phi }\to {G}=\left({x}\in {B},{y}\in {B}⟼{\mathrm{I}↾}_{\left({x}\mathrm{RingHom}{y}\right)}\right)$
8 5 adantr ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {U}\in \mathrm{WUni}$
9 eqid ${⊢}\mathrm{Hom}\left({R}\right)=\mathrm{Hom}\left({R}\right)$
10 simpr1 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}\in {B}$
11 simpr2 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Y}\in {B}$
12 1 3 8 9 10 11 ringchom ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}\mathrm{Hom}\left({R}\right){Y}={X}\mathrm{RingHom}{Y}$
13 12 eleq2d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left({H}\in \left({X}\mathrm{Hom}\left({R}\right){Y}\right)↔{H}\in \left({X}\mathrm{RingHom}{Y}\right)\right)$
14 simpr3 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Z}\in {B}$
15 1 3 8 9 11 14 ringchom ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Y}\mathrm{Hom}\left({R}\right){Z}={Y}\mathrm{RingHom}{Z}$
16 15 eleq2d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left({K}\in \left({Y}\mathrm{Hom}\left({R}\right){Z}\right)↔{K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)$
17 13 16 anbi12d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left(\left({H}\in \left({X}\mathrm{Hom}\left({R}\right){Y}\right)\wedge {K}\in \left({Y}\mathrm{Hom}\left({R}\right){Z}\right)\right)↔\left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)$
18 rhmco ${⊢}\left({K}\in \left({Y}\mathrm{RingHom}{Z}\right)\wedge {H}\in \left({X}\mathrm{RingHom}{Y}\right)\right)\to {K}\circ {H}\in \left({X}\mathrm{RingHom}{Z}\right)$
19 18 ancoms ${⊢}\left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\to {K}\circ {H}\in \left({X}\mathrm{RingHom}{Z}\right)$
20 19 adantl ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {K}\circ {H}\in \left({X}\mathrm{RingHom}{Z}\right)$
21 fvresi ${⊢}{K}\circ {H}\in \left({X}\mathrm{RingHom}{Z}\right)\to \left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Z}\right)}\right)\left({K}\circ {H}\right)={K}\circ {H}$
22 20 21 syl ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Z}\right)}\right)\left({K}\circ {H}\right)={K}\circ {H}$
23 1 2 3 4 5 6 7 funcringcsetcALTV2lem5 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}{G}{Z}={\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Z}\right)}$
24 23 3adantr2 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}{G}{Z}={\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Z}\right)}$
25 24 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {X}{G}{Z}={\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Z}\right)}$
26 8 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {U}\in \mathrm{WUni}$
27 eqid ${⊢}\mathrm{comp}\left({R}\right)=\mathrm{comp}\left({R}\right)$
28 1 3 5 ringcbas ${⊢}{\phi }\to {B}={U}\cap \mathrm{Ring}$
29 inss1 ${⊢}{U}\cap \mathrm{Ring}\subseteq {U}$
30 28 29 eqsstrdi ${⊢}{\phi }\to {B}\subseteq {U}$
31 30 sseld ${⊢}{\phi }\to \left({X}\in {B}\to {X}\in {U}\right)$
32 31 com12 ${⊢}{X}\in {B}\to \left({\phi }\to {X}\in {U}\right)$
33 32 3ad2ant1 ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\to \left({\phi }\to {X}\in {U}\right)$
34 33 impcom ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {X}\in {U}$
35 34 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {X}\in {U}$
36 30 sseld ${⊢}{\phi }\to \left({Y}\in {B}\to {Y}\in {U}\right)$
37 36 com12 ${⊢}{Y}\in {B}\to \left({\phi }\to {Y}\in {U}\right)$
38 37 3ad2ant2 ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\to \left({\phi }\to {Y}\in {U}\right)$
39 38 impcom ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Y}\in {U}$
40 39 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {Y}\in {U}$
41 30 sseld ${⊢}{\phi }\to \left({Z}\in {B}\to {Z}\in {U}\right)$
42 41 com12 ${⊢}{Z}\in {B}\to \left({\phi }\to {Z}\in {U}\right)$
43 42 3ad2ant3 ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\to \left({\phi }\to {Z}\in {U}\right)$
44 43 impcom ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {Z}\in {U}$
45 44 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {Z}\in {U}$
46 eqid ${⊢}{\mathrm{Base}}_{{X}}={\mathrm{Base}}_{{X}}$
47 eqid ${⊢}{\mathrm{Base}}_{{Y}}={\mathrm{Base}}_{{Y}}$
48 46 47 rhmf ${⊢}{H}\in \left({X}\mathrm{RingHom}{Y}\right)\to {H}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}$
49 48 ad2antrl ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {H}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}$
50 eqid ${⊢}{\mathrm{Base}}_{{Z}}={\mathrm{Base}}_{{Z}}$
51 47 50 rhmf ${⊢}{K}\in \left({Y}\mathrm{RingHom}{Z}\right)\to {K}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{Z}}$
52 51 ad2antll ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {K}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{Z}}$
53 1 26 27 35 40 45 49 52 ringcco ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({R}\right){Z}\right){H}={K}\circ {H}$
54 25 53 fveq12d ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({X}{G}{Z}\right)\left({K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({R}\right){Z}\right){H}\right)=\left({\mathrm{I}↾}_{\left({X}\mathrm{RingHom}{Z}\right)}\right)\left({K}\circ {H}\right)$
55 eqid ${⊢}\mathrm{comp}\left({S}\right)=\mathrm{comp}\left({S}\right)$
56 1 2 3 4 5 6 funcringcsetcALTV2lem2 ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {F}\left({X}\right)\in {U}$
57 56 3ad2antr1 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {F}\left({X}\right)\in {U}$
58 57 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {F}\left({X}\right)\in {U}$
59 1 2 3 4 5 6 funcringcsetcALTV2lem2 ${⊢}\left({\phi }\wedge {Y}\in {B}\right)\to {F}\left({Y}\right)\in {U}$
60 59 3ad2antr2 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {F}\left({Y}\right)\in {U}$
61 60 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {F}\left({Y}\right)\in {U}$
62 1 2 3 4 5 6 funcringcsetcALTV2lem2 ${⊢}\left({\phi }\wedge {Z}\in {B}\right)\to {F}\left({Z}\right)\in {U}$
63 62 3ad2antr3 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {F}\left({Z}\right)\in {U}$
64 63 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {F}\left({Z}\right)\in {U}$
65 1 2 3 4 5 6 funcringcsetcALTV2lem1 ${⊢}\left({\phi }\wedge {X}\in {B}\right)\to {F}\left({X}\right)={\mathrm{Base}}_{{X}}$
66 65 3ad2antr1 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {F}\left({X}\right)={\mathrm{Base}}_{{X}}$
67 1 2 3 4 5 6 funcringcsetcALTV2lem1 ${⊢}\left({\phi }\wedge {Y}\in {B}\right)\to {F}\left({Y}\right)={\mathrm{Base}}_{{Y}}$
68 67 3ad2antr2 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {F}\left({Y}\right)={\mathrm{Base}}_{{Y}}$
69 66 68 feq23d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left({H}:{F}\left({X}\right)⟶{F}\left({Y}\right)↔{H}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\right)$
70 69 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({H}:{F}\left({X}\right)⟶{F}\left({Y}\right)↔{H}:{\mathrm{Base}}_{{X}}⟶{\mathrm{Base}}_{{Y}}\right)$
71 49 70 mpbird ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {H}:{F}\left({X}\right)⟶{F}\left({Y}\right)$
72 simpll ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {\phi }$
73 3simpa ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\to \left({X}\in {B}\wedge {Y}\in {B}\right)$
74 73 ad2antlr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({X}\in {B}\wedge {Y}\in {B}\right)$
75 simprl ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {H}\in \left({X}\mathrm{RingHom}{Y}\right)$
76 1 2 3 4 5 6 7 funcringcsetcALTV2lem6 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\right)\wedge {H}\in \left({X}\mathrm{RingHom}{Y}\right)\right)\to \left({X}{G}{Y}\right)\left({H}\right)={H}$
77 72 74 75 76 syl3anc ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({X}{G}{Y}\right)\left({H}\right)={H}$
78 77 feq1d ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left(\left({X}{G}{Y}\right)\left({H}\right):{F}\left({X}\right)⟶{F}\left({Y}\right)↔{H}:{F}\left({X}\right)⟶{F}\left({Y}\right)\right)$
79 71 78 mpbird ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({X}{G}{Y}\right)\left({H}\right):{F}\left({X}\right)⟶{F}\left({Y}\right)$
80 1 2 3 4 5 6 funcringcsetcALTV2lem1 ${⊢}\left({\phi }\wedge {Z}\in {B}\right)\to {F}\left({Z}\right)={\mathrm{Base}}_{{Z}}$
81 80 3ad2antr3 ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to {F}\left({Z}\right)={\mathrm{Base}}_{{Z}}$
82 68 81 feq23d ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left({K}:{F}\left({Y}\right)⟶{F}\left({Z}\right)↔{K}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{Z}}\right)$
83 82 adantr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({K}:{F}\left({Y}\right)⟶{F}\left({Z}\right)↔{K}:{\mathrm{Base}}_{{Y}}⟶{\mathrm{Base}}_{{Z}}\right)$
84 52 83 mpbird ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {K}:{F}\left({Y}\right)⟶{F}\left({Z}\right)$
85 3simpc ${⊢}\left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\to \left({Y}\in {B}\wedge {Z}\in {B}\right)$
86 85 ad2antlr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({Y}\in {B}\wedge {Z}\in {B}\right)$
87 simprr ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to {K}\in \left({Y}\mathrm{RingHom}{Z}\right)$
88 1 2 3 4 5 6 7 funcringcsetcALTV2lem6 ${⊢}\left({\phi }\wedge \left({Y}\in {B}\wedge {Z}\in {B}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\to \left({Y}{G}{Z}\right)\left({K}\right)={K}$
89 72 86 87 88 syl3anc ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({Y}{G}{Z}\right)\left({K}\right)={K}$
90 89 feq1d ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left(\left({Y}{G}{Z}\right)\left({K}\right):{F}\left({Y}\right)⟶{F}\left({Z}\right)↔{K}:{F}\left({Y}\right)⟶{F}\left({Z}\right)\right)$
91 84 90 mpbird ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({Y}{G}{Z}\right)\left({K}\right):{F}\left({Y}\right)⟶{F}\left({Z}\right)$
92 2 26 55 58 61 64 79 91 setcco ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)=\left({Y}{G}{Z}\right)\left({K}\right)\circ \left({X}{G}{Y}\right)\left({H}\right)$
93 89 77 coeq12d ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({Y}{G}{Z}\right)\left({K}\right)\circ \left({X}{G}{Y}\right)\left({H}\right)={K}\circ {H}$
94 92 93 eqtrd ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)={K}\circ {H}$
95 22 54 94 3eqtr4d ${⊢}\left(\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\wedge \left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\right)\to \left({X}{G}{Z}\right)\left({K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({R}\right){Z}\right){H}\right)=\left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)$
96 95 ex ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left(\left({H}\in \left({X}\mathrm{RingHom}{Y}\right)\wedge {K}\in \left({Y}\mathrm{RingHom}{Z}\right)\right)\to \left({X}{G}{Z}\right)\left({K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({R}\right){Z}\right){H}\right)=\left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)\right)$
97 17 96 sylbid ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\right)\to \left(\left({H}\in \left({X}\mathrm{Hom}\left({R}\right){Y}\right)\wedge {K}\in \left({Y}\mathrm{Hom}\left({R}\right){Z}\right)\right)\to \left({X}{G}{Z}\right)\left({K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({R}\right){Z}\right){H}\right)=\left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)\right)$
98 97 3impia ${⊢}\left({\phi }\wedge \left({X}\in {B}\wedge {Y}\in {B}\wedge {Z}\in {B}\right)\wedge \left({H}\in \left({X}\mathrm{Hom}\left({R}\right){Y}\right)\wedge {K}\in \left({Y}\mathrm{Hom}\left({R}\right){Z}\right)\right)\right)\to \left({X}{G}{Z}\right)\left({K}\left(⟨{X},{Y}⟩\mathrm{comp}\left({R}\right){Z}\right){H}\right)=\left({Y}{G}{Z}\right)\left({K}\right)\left(⟨{F}\left({X}\right),{F}\left({Y}\right)⟩\mathrm{comp}\left({S}\right){F}\left({Z}\right)\right)\left({X}{G}{Y}\right)\left({H}\right)$