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 ⊢G∈GrpOp∧H∈GrpOp∧K∈GrpOp∧S∈GGrpOpHomH∧T∈HGrpOpHomK→T∘S∈GGrpOpHomK

Proof

Step Hyp Ref Expression
1 fco ⊢T:ran⁡H⟶ran⁡K∧S:ran⁡G⟶ran⁡H→T∘S:ran⁡G⟶ran⁡K
2 1 ancoms ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K→T∘S:ran⁡G⟶ran⁡K
3 2 ad2ant2r ⊢S:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv→T∘S:ran⁡G⟶ran⁡K
4 3 a1i ⊢G∈GrpOp∧H∈GrpOp∧K∈GrpOp→S:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv→T∘S:ran⁡G⟶ran⁡K
5 ffvelcdm ⊢S:ran⁡G⟶ran⁡H∧x∈ran⁡G→S⁡x∈ran⁡H
6 ffvelcdm ⊢S:ran⁡G⟶ran⁡H∧y∈ran⁡G→S⁡y∈ran⁡H
7 5 6 anim12dan ⊢S:ran⁡G⟶ran⁡H∧x∈ran⁡G∧y∈ran⁡G→S⁡x∈ran⁡H∧S⁡y∈ran⁡H
8 fveq2 ⊢u=S⁡x→T⁡u=T⁡S⁡x
9 8 oveq1d ⊢u=S⁡x→T⁡uKT⁡v=T⁡S⁡xKT⁡v
10 fvoveq1 ⊢u=S⁡x→T⁡uHv=T⁡S⁡xHv
11 9 10 eqeq12d ⊢u=S⁡x→T⁡uKT⁡v=T⁡uHv↔T⁡S⁡xKT⁡v=T⁡S⁡xHv
12 fveq2 ⊢v=S⁡y→T⁡v=T⁡S⁡y
13 12 oveq2d ⊢v=S⁡y→T⁡S⁡xKT⁡v=T⁡S⁡xKT⁡S⁡y
14 oveq2 ⊢v=S⁡y→S⁡xHv=S⁡xHS⁡y
15 14 fveq2d ⊢v=S⁡y→T⁡S⁡xHv=T⁡S⁡xHS⁡y
16 13 15 eqeq12d ⊢v=S⁡y→T⁡S⁡xKT⁡v=T⁡S⁡xHv↔T⁡S⁡xKT⁡S⁡y=T⁡S⁡xHS⁡y
17 11 16 rspc2va ⊢S⁡x∈ran⁡H∧S⁡y∈ran⁡H∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv→T⁡S⁡xKT⁡S⁡y=T⁡S⁡xHS⁡y
18 7 17 sylan ⊢S:ran⁡G⟶ran⁡H∧x∈ran⁡G∧y∈ran⁡G∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv→T⁡S⁡xKT⁡S⁡y=T⁡S⁡xHS⁡y
19 18 an32s ⊢S:ran⁡G⟶ran⁡H∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv∧x∈ran⁡G∧y∈ran⁡G→T⁡S⁡xKT⁡S⁡y=T⁡S⁡xHS⁡y
20 19 adantllr ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv∧x∈ran⁡G∧y∈ran⁡G→T⁡S⁡xKT⁡S⁡y=T⁡S⁡xHS⁡y
21 20 adantllr ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧G∈GrpOp∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv∧x∈ran⁡G∧y∈ran⁡G→T⁡S⁡xKT⁡S⁡y=T⁡S⁡xHS⁡y
22 fveq2 ⊢S⁡xHS⁡y=S⁡xGy→T⁡S⁡xHS⁡y=T⁡S⁡xGy
23 21 22 sylan9eq ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧G∈GrpOp∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv∧x∈ran⁡G∧y∈ran⁡G∧S⁡xHS⁡y=S⁡xGy→T⁡S⁡xKT⁡S⁡y=T⁡S⁡xGy
24 23 anasss ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧G∈GrpOp∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv∧x∈ran⁡G∧y∈ran⁡G∧S⁡xHS⁡y=S⁡xGy→T⁡S⁡xKT⁡S⁡y=T⁡S⁡xGy
25 fvco3 ⊢S:ran⁡G⟶ran⁡H∧x∈ran⁡G→T∘S⁡x=T⁡S⁡x
26 25 ad2ant2r ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧x∈ran⁡G∧y∈ran⁡G→T∘S⁡x=T⁡S⁡x
27 fvco3 ⊢S:ran⁡G⟶ran⁡H∧y∈ran⁡G→T∘S⁡y=T⁡S⁡y
28 27 ad2ant2rl ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧x∈ran⁡G∧y∈ran⁡G→T∘S⁡y=T⁡S⁡y
29 26 28 oveq12d ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧x∈ran⁡G∧y∈ran⁡G→T∘S⁡xKT∘S⁡y=T⁡S⁡xKT⁡S⁡y
30 29 adantlr ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧G∈GrpOp∧x∈ran⁡G∧y∈ran⁡G→T∘S⁡xKT∘S⁡y=T⁡S⁡xKT⁡S⁡y
31 30 ad2ant2r ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧G∈GrpOp∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv∧x∈ran⁡G∧y∈ran⁡G∧S⁡xHS⁡y=S⁡xGy→T∘S⁡xKT∘S⁡y=T⁡S⁡xKT⁡S⁡y
32 eqid ⊢ran⁡G=ran⁡G
33 32 grpocl ⊢G∈GrpOp∧x∈ran⁡G∧y∈ran⁡G→xGy∈ran⁡G
34 33 3expb ⊢G∈GrpOp∧x∈ran⁡G∧y∈ran⁡G→xGy∈ran⁡G
35 fvco3 ⊢S:ran⁡G⟶ran⁡H∧xGy∈ran⁡G→T∘S⁡xGy=T⁡S⁡xGy
36 35 adantlr ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧xGy∈ran⁡G→T∘S⁡xGy=T⁡S⁡xGy
37 34 36 sylan2 ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧G∈GrpOp∧x∈ran⁡G∧y∈ran⁡G→T∘S⁡xGy=T⁡S⁡xGy
38 37 anassrs ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧G∈GrpOp∧x∈ran⁡G∧y∈ran⁡G→T∘S⁡xGy=T⁡S⁡xGy
39 38 ad2ant2r ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧G∈GrpOp∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv∧x∈ran⁡G∧y∈ran⁡G∧S⁡xHS⁡y=S⁡xGy→T∘S⁡xGy=T⁡S⁡xGy
40 24 31 39 3eqtr4d ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧G∈GrpOp∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv∧x∈ran⁡G∧y∈ran⁡G∧S⁡xHS⁡y=S⁡xGy→T∘S⁡xKT∘S⁡y=T∘S⁡xGy
41 40 expr ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧G∈GrpOp∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv∧x∈ran⁡G∧y∈ran⁡G→S⁡xHS⁡y=S⁡xGy→T∘S⁡xKT∘S⁡y=T∘S⁡xGy
42 41 ralimdvva ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧G∈GrpOp∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv→∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy→∀x∈ran⁡G∀y∈ran⁡GT∘S⁡xKT∘S⁡y=T∘S⁡xGy
43 42 an32s ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv∧G∈GrpOp→∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy→∀x∈ran⁡G∀y∈ran⁡GT∘S⁡xKT∘S⁡y=T∘S⁡xGy
44 43 ex ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv→G∈GrpOp→∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy→∀x∈ran⁡G∀y∈ran⁡GT∘S⁡xKT∘S⁡y=T∘S⁡xGy
45 44 com23 ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv→∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy→G∈GrpOp→∀x∈ran⁡G∀y∈ran⁡GT∘S⁡xKT∘S⁡y=T∘S⁡xGy
46 45 anasss ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv→∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy→G∈GrpOp→∀x∈ran⁡G∀y∈ran⁡GT∘S⁡xKT∘S⁡y=T∘S⁡xGy
47 46 imp ⊢S:ran⁡G⟶ran⁡H∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv∧∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy→G∈GrpOp→∀x∈ran⁡G∀y∈ran⁡GT∘S⁡xKT∘S⁡y=T∘S⁡xGy
48 47 an32s ⊢S:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv→G∈GrpOp→∀x∈ran⁡G∀y∈ran⁡GT∘S⁡xKT∘S⁡y=T∘S⁡xGy
49 48 com12 ⊢G∈GrpOp→S:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv→∀x∈ran⁡G∀y∈ran⁡GT∘S⁡xKT∘S⁡y=T∘S⁡xGy
50 49 3ad2ant1 ⊢G∈GrpOp∧H∈GrpOp∧K∈GrpOp→S:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv→∀x∈ran⁡G∀y∈ran⁡GT∘S⁡xKT∘S⁡y=T∘S⁡xGy
51 4 50 jcad ⊢G∈GrpOp∧H∈GrpOp∧K∈GrpOp→S:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv→T∘S:ran⁡G⟶ran⁡K∧∀x∈ran⁡G∀y∈ran⁡GT∘S⁡xKT∘S⁡y=T∘S⁡xGy
52 eqid ⊢ran⁡H=ran⁡H
53 32 52 elghomOLD ⊢G∈GrpOp∧H∈GrpOp→S∈GGrpOpHomH↔S:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy
54 53 3adant3 ⊢G∈GrpOp∧H∈GrpOp∧K∈GrpOp→S∈GGrpOpHomH↔S:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy
55 eqid ⊢ran⁡K=ran⁡K
56 52 55 elghomOLD ⊢H∈GrpOp∧K∈GrpOp→T∈HGrpOpHomK↔T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv
57 56 3adant1 ⊢G∈GrpOp∧H∈GrpOp∧K∈GrpOp→T∈HGrpOpHomK↔T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv
58 54 57 anbi12d ⊢G∈GrpOp∧H∈GrpOp∧K∈GrpOp→S∈GGrpOpHomH∧T∈HGrpOpHomK↔S:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GS⁡xHS⁡y=S⁡xGy∧T:ran⁡H⟶ran⁡K∧∀u∈ran⁡H∀v∈ran⁡HT⁡uKT⁡v=T⁡uHv
59 32 55 elghomOLD ⊢G∈GrpOp∧K∈GrpOp→T∘S∈GGrpOpHomK↔T∘S:ran⁡G⟶ran⁡K∧∀x∈ran⁡G∀y∈ran⁡GT∘S⁡xKT∘S⁡y=T∘S⁡xGy
60 59 3adant2 ⊢G∈GrpOp∧H∈GrpOp∧K∈GrpOp→T∘S∈GGrpOpHomK↔T∘S:ran⁡G⟶ran⁡K∧∀x∈ran⁡G∀y∈ran⁡GT∘S⁡xKT∘S⁡y=T∘S⁡xGy
61 51 58 60 3imtr4d ⊢G∈GrpOp∧H∈GrpOp∧K∈GrpOp→S∈GGrpOpHomH∧T∈HGrpOpHomK→T∘S∈GGrpOpHomK
62 61 imp ⊢G∈GrpOp∧H∈GrpOp∧K∈GrpOp∧S∈GGrpOpHomH∧T∈HGrpOpHomK→T∘S∈GGrpOpHomK