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 ∈ G GrpOpHom H ∧ T ∈ H GrpOpHom K → T ∘ S ∈ G GrpOpHom K

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 ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v → 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 ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v → 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 ⁡ u K T ⁡ v = T ⁡ S ⁡ x K T ⁡ v
10 fvoveq1 ⊢ u = S ⁡ x → T ⁡ u H v = T ⁡ S ⁡ x H v
11 9 10 eqeq12d ⊢ u = S ⁡ x → T ⁡ u K T ⁡ v = T ⁡ u H v ↔ T ⁡ S ⁡ x K T ⁡ v = T ⁡ S ⁡ x H v
12 fveq2 ⊢ v = S ⁡ y → T ⁡ v = T ⁡ S ⁡ y
13 12 oveq2d ⊢ v = S ⁡ y → T ⁡ S ⁡ x K T ⁡ v = T ⁡ S ⁡ x K T ⁡ S ⁡ y
14 oveq2 ⊢ v = S ⁡ y → S ⁡ x H v = S ⁡ x H S ⁡ y
15 14 fveq2d ⊢ v = S ⁡ y → T ⁡ S ⁡ x H v = T ⁡ S ⁡ x H S ⁡ y
16 13 15 eqeq12d ⊢ v = S ⁡ y → T ⁡ S ⁡ x K T ⁡ v = T ⁡ S ⁡ x H v ↔ T ⁡ S ⁡ x K T ⁡ S ⁡ y = T ⁡ S ⁡ x H S ⁡ y
17 11 16 rspc2va ⊢ S ⁡ x ∈ ran ⁡ H ∧ S ⁡ y ∈ ran ⁡ H ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v → T ⁡ S ⁡ x K T ⁡ S ⁡ y = T ⁡ S ⁡ x H S ⁡ y
18 7 17 sylan ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v → T ⁡ S ⁡ x K T ⁡ S ⁡ y = T ⁡ S ⁡ x H S ⁡ y
19 18 an32s ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G → T ⁡ S ⁡ x K T ⁡ S ⁡ y = T ⁡ S ⁡ x H S ⁡ y
20 19 adantllr ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G → T ⁡ S ⁡ x K T ⁡ S ⁡ y = T ⁡ S ⁡ x H S ⁡ y
21 20 adantllr ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ G ∈ GrpOp ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G → T ⁡ S ⁡ x K T ⁡ S ⁡ y = T ⁡ S ⁡ x H S ⁡ y
22 fveq2 ⊢ S ⁡ x H S ⁡ y = S ⁡ x G y → T ⁡ S ⁡ x H S ⁡ y = T ⁡ S ⁡ x G y
23 21 22 sylan9eq ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ G ∈ GrpOp ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G ∧ S ⁡ x H S ⁡ y = S ⁡ x G y → T ⁡ S ⁡ x K T ⁡ S ⁡ y = T ⁡ S ⁡ x G y
24 23 anasss ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ G ∈ GrpOp ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G ∧ S ⁡ x H S ⁡ y = S ⁡ x G y → T ⁡ S ⁡ x K T ⁡ S ⁡ y = T ⁡ S ⁡ x G y
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 ⁡ x K T ∘ S ⁡ y = T ⁡ S ⁡ x K T ⁡ 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 ⁡ x K T ∘ S ⁡ y = T ⁡ S ⁡ x K T ⁡ S ⁡ y
31 30 ad2ant2r ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ G ∈ GrpOp ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G ∧ S ⁡ x H S ⁡ y = S ⁡ x G y → T ∘ S ⁡ x K T ∘ S ⁡ y = T ⁡ S ⁡ x K T ⁡ S ⁡ y
32 eqid ⊢ ran ⁡ G = ran ⁡ G
33 32 grpocl ⊢ G ∈ GrpOp ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G → x G y ∈ ran ⁡ G
34 33 3expb ⊢ G ∈ GrpOp ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G → x G y ∈ ran ⁡ G
35 fvco3 ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ x G y ∈ ran ⁡ G → T ∘ S ⁡ x G y = T ⁡ S ⁡ x G y
36 35 adantlr ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ x G y ∈ ran ⁡ G → T ∘ S ⁡ x G y = T ⁡ S ⁡ x G y
37 34 36 sylan2 ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ G ∈ GrpOp ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G → T ∘ S ⁡ x G y = T ⁡ S ⁡ x G y
38 37 anassrs ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ G ∈ GrpOp ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G → T ∘ S ⁡ x G y = T ⁡ S ⁡ x G y
39 38 ad2ant2r ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ G ∈ GrpOp ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G ∧ S ⁡ x H S ⁡ y = S ⁡ x G y → T ∘ S ⁡ x G y = T ⁡ S ⁡ x G y
40 24 31 39 3eqtr4d ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ G ∈ GrpOp ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G ∧ S ⁡ x H S ⁡ y = S ⁡ x G y → T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
41 40 expr ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ G ∈ GrpOp ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v ∧ x ∈ ran ⁡ G ∧ y ∈ ran ⁡ G → S ⁡ x H S ⁡ y = S ⁡ x G y → T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
42 41 ralimdvva ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ G ∈ GrpOp ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
43 42 an32s ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v ∧ G ∈ GrpOp → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
44 43 ex ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v → G ∈ GrpOp → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
45 44 com23 ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y → G ∈ GrpOp → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
46 45 anasss ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y → G ∈ GrpOp → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
47 46 imp ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y → G ∈ GrpOp → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
48 47 an32s ⊢ S : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v → G ∈ GrpOp → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
49 48 com12 ⊢ G ∈ GrpOp → S : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
50 49 3ad2ant1 ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ K ∈ GrpOp → S : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v → ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
51 4 50 jcad ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ K ∈ GrpOp → S : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v → T ∘ S : ran ⁡ G ⟶ ran ⁡ K ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
52 eqid ⊢ ran ⁡ H = ran ⁡ H
53 32 52 elghomOLD ⊢ G ∈ GrpOp ∧ H ∈ GrpOp → S ∈ G GrpOpHom H ↔ S : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y
54 53 3adant3 ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ K ∈ GrpOp → S ∈ G GrpOpHom H ↔ S : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y
55 eqid ⊢ ran ⁡ K = ran ⁡ K
56 52 55 elghomOLD ⊢ H ∈ GrpOp ∧ K ∈ GrpOp → T ∈ H GrpOpHom K ↔ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v
57 56 3adant1 ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ K ∈ GrpOp → T ∈ H GrpOpHom K ↔ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v
58 54 57 anbi12d ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ K ∈ GrpOp → S ∈ G GrpOpHom H ∧ T ∈ H GrpOpHom K ↔ S : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G S ⁡ x H S ⁡ y = S ⁡ x G y ∧ T : ran ⁡ H ⟶ ran ⁡ K ∧ ∀ u ∈ ran ⁡ H ∀ v ∈ ran ⁡ H T ⁡ u K T ⁡ v = T ⁡ u H v
59 32 55 elghomOLD ⊢ G ∈ GrpOp ∧ K ∈ GrpOp → T ∘ S ∈ G GrpOpHom K ↔ T ∘ S : ran ⁡ G ⟶ ran ⁡ K ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
60 59 3adant2 ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ K ∈ GrpOp → T ∘ S ∈ G GrpOpHom K ↔ T ∘ S : ran ⁡ G ⟶ ran ⁡ K ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G T ∘ S ⁡ x K T ∘ S ⁡ y = T ∘ S ⁡ x G y
61 51 58 60 3imtr4d ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ K ∈ GrpOp → S ∈ G GrpOpHom H ∧ T ∈ H GrpOpHom K → T ∘ S ∈ G GrpOpHom K
62 61 imp ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ K ∈ GrpOp ∧ S ∈ G GrpOpHom H ∧ T ∈ H GrpOpHom K → T ∘ S ∈ G GrpOpHom K