# Metamath Proof Explorer

## Theorem ghomco

Description: The composition of two group homomorphisms is a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009) (Revised by Mario Carneiro, 27-Dec-2014)

Ref Expression
Assertion ghomco ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {K}\in \mathrm{GrpOp}\right)\wedge \left({S}\in \left({G}\mathrm{GrpOpHom}{H}\right)\wedge {T}\in \left({H}\mathrm{GrpOpHom}{K}\right)\right)\right)\to {T}\circ {S}\in \left({G}\mathrm{GrpOpHom}{K}\right)$

### Proof

Step Hyp Ref Expression
1 fco ${⊢}\left({T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\wedge {S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\right)\to \left({T}\circ {S}\right):\mathrm{ran}{G}⟶\mathrm{ran}{K}$
2 1 ancoms ${⊢}\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\to \left({T}\circ {S}\right):\mathrm{ran}{G}⟶\mathrm{ran}{K}$
3 2 ad2ant2r ${⊢}\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\wedge \left({T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\right)\to \left({T}\circ {S}\right):\mathrm{ran}{G}⟶\mathrm{ran}{K}$
4 3 a1i ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {K}\in \mathrm{GrpOp}\right)\to \left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\wedge \left({T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\right)\to \left({T}\circ {S}\right):\mathrm{ran}{G}⟶\mathrm{ran}{K}\right)$
5 ffvelrn ${⊢}\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {x}\in \mathrm{ran}{G}\right)\to {S}\left({x}\right)\in \mathrm{ran}{H}$
6 ffvelrn ${⊢}\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {y}\in \mathrm{ran}{G}\right)\to {S}\left({y}\right)\in \mathrm{ran}{H}$
7 5 6 anim12dan ${⊢}\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\to \left({S}\left({x}\right)\in \mathrm{ran}{H}\wedge {S}\left({y}\right)\in \mathrm{ran}{H}\right)$
8 fveq2 ${⊢}{u}={S}\left({x}\right)\to {T}\left({u}\right)={T}\left({S}\left({x}\right)\right)$
9 8 oveq1d ${⊢}{u}={S}\left({x}\right)\to {T}\left({u}\right){K}{T}\left({v}\right)={T}\left({S}\left({x}\right)\right){K}{T}\left({v}\right)$
10 fvoveq1 ${⊢}{u}={S}\left({x}\right)\to {T}\left({u}{H}{v}\right)={T}\left({S}\left({x}\right){H}{v}\right)$
11 9 10 eqeq12d ${⊢}{u}={S}\left({x}\right)\to \left({T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)↔{T}\left({S}\left({x}\right)\right){K}{T}\left({v}\right)={T}\left({S}\left({x}\right){H}{v}\right)\right)$
12 fveq2 ${⊢}{v}={S}\left({y}\right)\to {T}\left({v}\right)={T}\left({S}\left({y}\right)\right)$
13 12 oveq2d ${⊢}{v}={S}\left({y}\right)\to {T}\left({S}\left({x}\right)\right){K}{T}\left({v}\right)={T}\left({S}\left({x}\right)\right){K}{T}\left({S}\left({y}\right)\right)$
14 oveq2 ${⊢}{v}={S}\left({y}\right)\to {S}\left({x}\right){H}{v}={S}\left({x}\right){H}{S}\left({y}\right)$
15 14 fveq2d ${⊢}{v}={S}\left({y}\right)\to {T}\left({S}\left({x}\right){H}{v}\right)={T}\left({S}\left({x}\right){H}{S}\left({y}\right)\right)$
16 13 15 eqeq12d ${⊢}{v}={S}\left({y}\right)\to \left({T}\left({S}\left({x}\right)\right){K}{T}\left({v}\right)={T}\left({S}\left({x}\right){H}{v}\right)↔{T}\left({S}\left({x}\right)\right){K}{T}\left({S}\left({y}\right)\right)={T}\left({S}\left({x}\right){H}{S}\left({y}\right)\right)\right)$
17 11 16 rspc2va ${⊢}\left(\left({S}\left({x}\right)\in \mathrm{ran}{H}\wedge {S}\left({y}\right)\in \mathrm{ran}{H}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\to {T}\left({S}\left({x}\right)\right){K}{T}\left({S}\left({y}\right)\right)={T}\left({S}\left({x}\right){H}{S}\left({y}\right)\right)$
18 7 17 sylan ${⊢}\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\to {T}\left({S}\left({x}\right)\right){K}{T}\left({S}\left({y}\right)\right)={T}\left({S}\left({x}\right){H}{S}\left({y}\right)\right)$
19 18 an32s ${⊢}\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\to {T}\left({S}\left({x}\right)\right){K}{T}\left({S}\left({y}\right)\right)={T}\left({S}\left({x}\right){H}{S}\left({y}\right)\right)$
20 19 adantllr ${⊢}\left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\to {T}\left({S}\left({x}\right)\right){K}{T}\left({S}\left({y}\right)\right)={T}\left({S}\left({x}\right){H}{S}\left({y}\right)\right)$
21 20 adantllr ${⊢}\left(\left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge {G}\in \mathrm{GrpOp}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\to {T}\left({S}\left({x}\right)\right){K}{T}\left({S}\left({y}\right)\right)={T}\left({S}\left({x}\right){H}{S}\left({y}\right)\right)$
22 fveq2 ${⊢}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\to {T}\left({S}\left({x}\right){H}{S}\left({y}\right)\right)={T}\left({S}\left({x}{G}{y}\right)\right)$
23 21 22 sylan9eq ${⊢}\left(\left(\left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge {G}\in \mathrm{GrpOp}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\wedge {S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\to {T}\left({S}\left({x}\right)\right){K}{T}\left({S}\left({y}\right)\right)={T}\left({S}\left({x}{G}{y}\right)\right)$
24 23 anasss ${⊢}\left(\left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge {G}\in \mathrm{GrpOp}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\wedge \left(\left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\wedge {S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\right)\to {T}\left({S}\left({x}\right)\right){K}{T}\left({S}\left({y}\right)\right)={T}\left({S}\left({x}{G}{y}\right)\right)$
25 fvco3 ${⊢}\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {x}\in \mathrm{ran}{G}\right)\to \left({T}\circ {S}\right)\left({x}\right)={T}\left({S}\left({x}\right)\right)$
26 25 ad2ant2r ${⊢}\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\to \left({T}\circ {S}\right)\left({x}\right)={T}\left({S}\left({x}\right)\right)$
27 fvco3 ${⊢}\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {y}\in \mathrm{ran}{G}\right)\to \left({T}\circ {S}\right)\left({y}\right)={T}\left({S}\left({y}\right)\right)$
28 27 ad2ant2rl ${⊢}\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\to \left({T}\circ {S}\right)\left({y}\right)={T}\left({S}\left({y}\right)\right)$
29 26 28 oveq12d ${⊢}\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\to \left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)={T}\left({S}\left({x}\right)\right){K}{T}\left({S}\left({y}\right)\right)$
30 29 adantlr ${⊢}\left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge {G}\in \mathrm{GrpOp}\right)\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\to \left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)={T}\left({S}\left({x}\right)\right){K}{T}\left({S}\left({y}\right)\right)$
31 30 ad2ant2r ${⊢}\left(\left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge {G}\in \mathrm{GrpOp}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\wedge \left(\left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\wedge {S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\right)\to \left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)={T}\left({S}\left({x}\right)\right){K}{T}\left({S}\left({y}\right)\right)$
32 eqid ${⊢}\mathrm{ran}{G}=\mathrm{ran}{G}$
33 32 grpocl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\to {x}{G}{y}\in \mathrm{ran}{G}$
34 33 3expb ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\to {x}{G}{y}\in \mathrm{ran}{G}$
35 fvco3 ${⊢}\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {x}{G}{y}\in \mathrm{ran}{G}\right)\to \left({T}\circ {S}\right)\left({x}{G}{y}\right)={T}\left({S}\left({x}{G}{y}\right)\right)$
36 35 adantlr ${⊢}\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge {x}{G}{y}\in \mathrm{ran}{G}\right)\to \left({T}\circ {S}\right)\left({x}{G}{y}\right)={T}\left({S}\left({x}{G}{y}\right)\right)$
37 34 36 sylan2 ${⊢}\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge \left({G}\in \mathrm{GrpOp}\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\right)\to \left({T}\circ {S}\right)\left({x}{G}{y}\right)={T}\left({S}\left({x}{G}{y}\right)\right)$
38 37 anassrs ${⊢}\left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge {G}\in \mathrm{GrpOp}\right)\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\to \left({T}\circ {S}\right)\left({x}{G}{y}\right)={T}\left({S}\left({x}{G}{y}\right)\right)$
39 38 ad2ant2r ${⊢}\left(\left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge {G}\in \mathrm{GrpOp}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\wedge \left(\left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\wedge {S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\right)\to \left({T}\circ {S}\right)\left({x}{G}{y}\right)={T}\left({S}\left({x}{G}{y}\right)\right)$
40 24 31 39 3eqtr4d ${⊢}\left(\left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge {G}\in \mathrm{GrpOp}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\wedge \left(\left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\wedge {S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\right)\to \left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)$
41 40 expr ${⊢}\left(\left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge {G}\in \mathrm{GrpOp}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\wedge \left({x}\in \mathrm{ran}{G}\wedge {y}\in \mathrm{ran}{G}\right)\right)\to \left({S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\to \left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)$
42 41 ralimdvva ${⊢}\left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge {G}\in \mathrm{GrpOp}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\to \left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\to \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)$
43 42 an32s ${⊢}\left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\wedge {G}\in \mathrm{GrpOp}\right)\to \left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\to \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)$
44 43 ex ${⊢}\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\to \left({G}\in \mathrm{GrpOp}\to \left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\to \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)\right)$
45 44 com23 ${⊢}\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge {T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\right)\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\to \left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\to \left({G}\in \mathrm{GrpOp}\to \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)\right)$
46 45 anasss ${⊢}\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \left({T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\right)\to \left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\to \left({G}\in \mathrm{GrpOp}\to \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)\right)$
47 46 imp ${⊢}\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \left({T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\right)\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\to \left({G}\in \mathrm{GrpOp}\to \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)$
48 47 an32s ${⊢}\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\wedge \left({T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\right)\to \left({G}\in \mathrm{GrpOp}\to \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)$
49 48 com12 ${⊢}{G}\in \mathrm{GrpOp}\to \left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\wedge \left({T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\right)\to \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)$
50 49 3ad2ant1 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {K}\in \mathrm{GrpOp}\right)\to \left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\wedge \left({T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\right)\to \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)$
51 4 50 jcad ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {K}\in \mathrm{GrpOp}\right)\to \left(\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\wedge \left({T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\right)\to \left(\left({T}\circ {S}\right):\mathrm{ran}{G}⟶\mathrm{ran}{K}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)\right)$
52 eqid ${⊢}\mathrm{ran}{H}=\mathrm{ran}{H}$
53 32 52 elghomOLD ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\right)\to \left({S}\in \left({G}\mathrm{GrpOpHom}{H}\right)↔\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\right)$
54 53 3adant3 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {K}\in \mathrm{GrpOp}\right)\to \left({S}\in \left({G}\mathrm{GrpOpHom}{H}\right)↔\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\right)$
55 eqid ${⊢}\mathrm{ran}{K}=\mathrm{ran}{K}$
56 52 55 elghomOLD ${⊢}\left({H}\in \mathrm{GrpOp}\wedge {K}\in \mathrm{GrpOp}\right)\to \left({T}\in \left({H}\mathrm{GrpOpHom}{K}\right)↔\left({T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\right)$
57 56 3adant1 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {K}\in \mathrm{GrpOp}\right)\to \left({T}\in \left({H}\mathrm{GrpOpHom}{K}\right)↔\left({T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\right)$
58 54 57 anbi12d ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {K}\in \mathrm{GrpOp}\right)\to \left(\left({S}\in \left({G}\mathrm{GrpOpHom}{H}\right)\wedge {T}\in \left({H}\mathrm{GrpOpHom}{K}\right)\right)↔\left(\left({S}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{S}\left({x}\right){H}{S}\left({y}\right)={S}\left({x}{G}{y}\right)\right)\wedge \left({T}:\mathrm{ran}{H}⟶\mathrm{ran}{K}\wedge \forall {u}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}\forall {v}\in \mathrm{ran}{H}\phantom{\rule{.4em}{0ex}}{T}\left({u}\right){K}{T}\left({v}\right)={T}\left({u}{H}{v}\right)\right)\right)\right)$
59 32 55 elghomOLD ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {K}\in \mathrm{GrpOp}\right)\to \left({T}\circ {S}\in \left({G}\mathrm{GrpOpHom}{K}\right)↔\left(\left({T}\circ {S}\right):\mathrm{ran}{G}⟶\mathrm{ran}{K}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)\right)$
60 59 3adant2 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {K}\in \mathrm{GrpOp}\right)\to \left({T}\circ {S}\in \left({G}\mathrm{GrpOpHom}{K}\right)↔\left(\left({T}\circ {S}\right):\mathrm{ran}{G}⟶\mathrm{ran}{K}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({T}\circ {S}\right)\left({x}\right){K}\left({T}\circ {S}\right)\left({y}\right)=\left({T}\circ {S}\right)\left({x}{G}{y}\right)\right)\right)$
61 51 58 60 3imtr4d ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {K}\in \mathrm{GrpOp}\right)\to \left(\left({S}\in \left({G}\mathrm{GrpOpHom}{H}\right)\wedge {T}\in \left({H}\mathrm{GrpOpHom}{K}\right)\right)\to {T}\circ {S}\in \left({G}\mathrm{GrpOpHom}{K}\right)\right)$
62 61 imp ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {K}\in \mathrm{GrpOp}\right)\wedge \left({S}\in \left({G}\mathrm{GrpOpHom}{H}\right)\wedge {T}\in \left({H}\mathrm{GrpOpHom}{K}\right)\right)\right)\to {T}\circ {S}\in \left({G}\mathrm{GrpOpHom}{K}\right)$