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 e. GrpOp /\ H e. GrpOp /\ K e. GrpOp ) /\ ( S e. ( G GrpOpHom H ) /\ T e. ( H GrpOpHom K ) ) ) -> ( T o. S ) e. ( G GrpOpHom K ) )

Proof

Step Hyp Ref Expression
1 fco 
 |-  ( ( T : ran H --> ran K /\ S : ran G --> ran H ) -> ( T o. S ) : ran G --> ran K )
2 1 ancoms 
 |-  ( ( S : ran G --> ran H /\ T : ran H --> ran K ) -> ( T o. S ) : ran G --> ran K )
3 2 ad2ant2r 
 |-  ( ( ( S : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) /\ ( T : ran H --> ran K /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) ) -> ( T o. S ) : ran G --> ran K )
4 3 a1i 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ K e. GrpOp ) -> ( ( ( S : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) /\ ( T : ran H --> ran K /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) ) -> ( T o. S ) : ran G --> ran K ) )
5 ffvelrn 
 |-  ( ( S : ran G --> ran H /\ x e. ran G ) -> ( S ` x ) e. ran H )
6 ffvelrn 
 |-  ( ( S : ran G --> ran H /\ y e. ran G ) -> ( S ` y ) e. ran H )
7 5 6 anim12dan 
 |-  ( ( S : ran G --> ran H /\ ( x e. ran G /\ y e. ran G ) ) -> ( ( S ` x ) e. ran H /\ ( S ` y ) e. 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 ) e. ran H /\ ( S ` y ) e. ran H ) /\ A. u e. ran H A. v e. 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 e. ran G /\ y e. ran G ) ) /\ A. u e. ran H A. v e. 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 /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) /\ ( x e. ran G /\ y e. 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 ) /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) /\ ( x e. ran G /\ y e. 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 e. GrpOp ) /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) /\ ( x e. ran G /\ y e. 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 e. GrpOp ) /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) /\ ( x e. ran G /\ y e. 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 e. GrpOp ) /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) /\ ( ( x e. ran G /\ y e. 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 e. ran G ) -> ( ( T o. S ) ` x ) = ( T ` ( S ` x ) ) )
26 25 ad2ant2r 
 |-  ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ ( x e. ran G /\ y e. ran G ) ) -> ( ( T o. S ) ` x ) = ( T ` ( S ` x ) ) )
27 fvco3 
 |-  ( ( S : ran G --> ran H /\ y e. ran G ) -> ( ( T o. S ) ` y ) = ( T ` ( S ` y ) ) )
28 27 ad2ant2rl 
 |-  ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ ( x e. ran G /\ y e. ran G ) ) -> ( ( T o. S ) ` y ) = ( T ` ( S ` y ) ) )
29 26 28 oveq12d 
 |-  ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ ( x e. ran G /\ y e. ran G ) ) -> ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T ` ( S ` x ) ) K ( T ` ( S ` y ) ) ) )
30 29 adantlr 
 |-  ( ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ G e. GrpOp ) /\ ( x e. ran G /\ y e. ran G ) ) -> ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T ` ( S ` x ) ) K ( T ` ( S ` y ) ) ) )
31 30 ad2ant2r 
 |-  ( ( ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ G e. GrpOp ) /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) /\ ( ( x e. ran G /\ y e. ran G ) /\ ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) ) -> ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T ` ( S ` x ) ) K ( T ` ( S ` y ) ) ) )
32 eqid 
 |-  ran G = ran G
33 32 grpocl 
 |-  ( ( G e. GrpOp /\ x e. ran G /\ y e. ran G ) -> ( x G y ) e. ran G )
34 33 3expb 
 |-  ( ( G e. GrpOp /\ ( x e. ran G /\ y e. ran G ) ) -> ( x G y ) e. ran G )
35 fvco3 
 |-  ( ( S : ran G --> ran H /\ ( x G y ) e. ran G ) -> ( ( T o. 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 ) e. ran G ) -> ( ( T o. S ) ` ( x G y ) ) = ( T ` ( S ` ( x G y ) ) ) )
37 34 36 sylan2 
 |-  ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ ( G e. GrpOp /\ ( x e. ran G /\ y e. ran G ) ) ) -> ( ( T o. S ) ` ( x G y ) ) = ( T ` ( S ` ( x G y ) ) ) )
38 37 anassrs 
 |-  ( ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ G e. GrpOp ) /\ ( x e. ran G /\ y e. ran G ) ) -> ( ( T o. S ) ` ( x G y ) ) = ( T ` ( S ` ( x G y ) ) ) )
39 38 ad2ant2r 
 |-  ( ( ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ G e. GrpOp ) /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) /\ ( ( x e. ran G /\ y e. ran G ) /\ ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) ) -> ( ( T o. 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 e. GrpOp ) /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) /\ ( ( x e. ran G /\ y e. ran G ) /\ ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) ) -> ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) )
41 40 expr 
 |-  ( ( ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ G e. GrpOp ) /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) /\ ( x e. ran G /\ y e. ran G ) ) -> ( ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) -> ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) )
42 41 ralimdvva 
 |-  ( ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ G e. GrpOp ) /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) -> ( A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) -> A. x e. ran G A. y e. ran G ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) )
43 42 an32s 
 |-  ( ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) /\ G e. GrpOp ) -> ( A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) -> A. x e. ran G A. y e. ran G ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) )
44 43 ex 
 |-  ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) -> ( G e. GrpOp -> ( A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) -> A. x e. ran G A. y e. ran G ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) ) )
45 44 com23 
 |-  ( ( ( S : ran G --> ran H /\ T : ran H --> ran K ) /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) -> ( A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) -> ( G e. GrpOp -> A. x e. ran G A. y e. ran G ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) ) )
46 45 anasss 
 |-  ( ( S : ran G --> ran H /\ ( T : ran H --> ran K /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) ) -> ( A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) -> ( G e. GrpOp -> A. x e. ran G A. y e. ran G ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) ) )
47 46 imp 
 |-  ( ( ( S : ran G --> ran H /\ ( T : ran H --> ran K /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) ) /\ A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) -> ( G e. GrpOp -> A. x e. ran G A. y e. ran G ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) )
48 47 an32s 
 |-  ( ( ( S : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) /\ ( T : ran H --> ran K /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) ) -> ( G e. GrpOp -> A. x e. ran G A. y e. ran G ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) )
49 48 com12 
 |-  ( G e. GrpOp -> ( ( ( S : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) /\ ( T : ran H --> ran K /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) ) -> A. x e. ran G A. y e. ran G ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) )
50 49 3ad2ant1 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ K e. GrpOp ) -> ( ( ( S : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) /\ ( T : ran H --> ran K /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) ) -> A. x e. ran G A. y e. ran G ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) )
51 4 50 jcad 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ K e. GrpOp ) -> ( ( ( S : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) /\ ( T : ran H --> ran K /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) ) -> ( ( T o. S ) : ran G --> ran K /\ A. x e. ran G A. y e. ran G ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) ) )
52 eqid 
 |-  ran H = ran H
53 32 52 elghomOLD 
 |-  ( ( G e. GrpOp /\ H e. GrpOp ) -> ( S e. ( G GrpOpHom H ) <-> ( S : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) ) )
54 53 3adant3 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ K e. GrpOp ) -> ( S e. ( G GrpOpHom H ) <-> ( S : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) ) )
55 eqid 
 |-  ran K = ran K
56 52 55 elghomOLD 
 |-  ( ( H e. GrpOp /\ K e. GrpOp ) -> ( T e. ( H GrpOpHom K ) <-> ( T : ran H --> ran K /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) ) )
57 56 3adant1 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ K e. GrpOp ) -> ( T e. ( H GrpOpHom K ) <-> ( T : ran H --> ran K /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) ) )
58 54 57 anbi12d 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ K e. GrpOp ) -> ( ( S e. ( G GrpOpHom H ) /\ T e. ( H GrpOpHom K ) ) <-> ( ( S : ran G --> ran H /\ A. x e. ran G A. y e. ran G ( ( S ` x ) H ( S ` y ) ) = ( S ` ( x G y ) ) ) /\ ( T : ran H --> ran K /\ A. u e. ran H A. v e. ran H ( ( T ` u ) K ( T ` v ) ) = ( T ` ( u H v ) ) ) ) ) )
59 32 55 elghomOLD 
 |-  ( ( G e. GrpOp /\ K e. GrpOp ) -> ( ( T o. S ) e. ( G GrpOpHom K ) <-> ( ( T o. S ) : ran G --> ran K /\ A. x e. ran G A. y e. ran G ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) ) )
60 59 3adant2 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ K e. GrpOp ) -> ( ( T o. S ) e. ( G GrpOpHom K ) <-> ( ( T o. S ) : ran G --> ran K /\ A. x e. ran G A. y e. ran G ( ( ( T o. S ) ` x ) K ( ( T o. S ) ` y ) ) = ( ( T o. S ) ` ( x G y ) ) ) ) )
61 51 58 60 3imtr4d 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ K e. GrpOp ) -> ( ( S e. ( G GrpOpHom H ) /\ T e. ( H GrpOpHom K ) ) -> ( T o. S ) e. ( G GrpOpHom K ) ) )
62 61 imp 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ K e. GrpOp ) /\ ( S e. ( G GrpOpHom H ) /\ T e. ( H GrpOpHom K ) ) ) -> ( T o. S ) e. ( G GrpOpHom K ) )