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 ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp ) ∧ ( 𝑆 ∈ ( 𝐺 GrpOpHom 𝐻 ) ∧ 𝑇 ∈ ( 𝐻 GrpOpHom 𝐾 ) ) ) → ( 𝑇 ∘ 𝑆 ) ∈ ( 𝐺 GrpOpHom 𝐾 ) )

Proof

Step Hyp Ref Expression
1 fco ⊢ ( ( 𝑇 : ran 𝐻 ⟶ ran 𝐾 ∧ 𝑆 : ran 𝐺 ⟶ ran 𝐻 ) → ( 𝑇 ∘ 𝑆 ) : ran 𝐺 ⟶ ran 𝐾 )
2 1 ancoms ⊢ ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) → ( 𝑇 ∘ 𝑆 ) : ran 𝐺 ⟶ ran 𝐾 )
3 2 ad2ant2r ⊢ ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ∧ ( 𝑇 : ran 𝐻 ⟶ ran 𝐾 ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ) → ( 𝑇 ∘ 𝑆 ) : ran 𝐺 ⟶ ran 𝐾 )
4 3 a1i ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp ) → ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ∧ ( 𝑇 : ran 𝐻 ⟶ ran 𝐾 ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ) → ( 𝑇 ∘ 𝑆 ) : ran 𝐺 ⟶ ran 𝐾 ) )
5 ffvelrn ⊢ ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑥 ∈ ran 𝐺 ) → ( 𝑆 ‘ 𝑥 ) ∈ ran 𝐻 )
6 ffvelrn ⊢ ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑦 ∈ ran 𝐺 ) → ( 𝑆 ‘ 𝑦 ) ∈ ran 𝐻 )
7 5 6 anim12dan ⊢ ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( ( 𝑆 ‘ 𝑥 ) ∈ ran 𝐻 ∧ ( 𝑆 ‘ 𝑦 ) ∈ ran 𝐻 ) )
8 fveq2 ⊢ ( 𝑢 = ( 𝑆 ‘ 𝑥 ) → ( 𝑇 ‘ 𝑢 ) = ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) )
9 8 oveq1d ⊢ ( 𝑢 = ( 𝑆 ‘ 𝑥 ) → ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) )
10 fvoveq1 ⊢ ( 𝑢 = ( 𝑆 ‘ 𝑥 ) → ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) = ( 𝑇 ‘ ( ( 𝑆 ‘ 𝑥 ) 𝐻 𝑣 ) ) )
11 9 10 eqeq12d ⊢ ( 𝑢 = ( 𝑆 ‘ 𝑥 ) → ( ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ↔ ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( ( 𝑆 ‘ 𝑥 ) 𝐻 𝑣 ) ) ) )
12 fveq2 ⊢ ( 𝑣 = ( 𝑆 ‘ 𝑦 ) → ( 𝑇 ‘ 𝑣 ) = ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) )
13 12 oveq2d ⊢ ( 𝑣 = ( 𝑆 ‘ 𝑦 ) → ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
14 oveq2 ⊢ ( 𝑣 = ( 𝑆 ‘ 𝑦 ) → ( ( 𝑆 ‘ 𝑥 ) 𝐻 𝑣 ) = ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) )
15 14 fveq2d ⊢ ( 𝑣 = ( 𝑆 ‘ 𝑦 ) → ( 𝑇 ‘ ( ( 𝑆 ‘ 𝑥 ) 𝐻 𝑣 ) ) = ( 𝑇 ‘ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) ) )
16 13 15 eqeq12d ⊢ ( 𝑣 = ( 𝑆 ‘ 𝑦 ) → ( ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( ( 𝑆 ‘ 𝑥 ) 𝐻 𝑣 ) ) ↔ ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) = ( 𝑇 ‘ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) ) ) )
17 11 16 rspc2va ⊢ ( ( ( ( 𝑆 ‘ 𝑥 ) ∈ ran 𝐻 ∧ ( 𝑆 ‘ 𝑦 ) ∈ ran 𝐻 ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) → ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) = ( 𝑇 ‘ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) ) )
18 7 17 sylan ⊢ ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) → ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) = ( 𝑇 ‘ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) ) )
19 18 an32s ⊢ ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) = ( 𝑇 ‘ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) ) )
20 19 adantllr ⊢ ( ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) = ( 𝑇 ‘ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) ) )
21 20 adantllr ⊢ ( ( ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ 𝐺 ∈ GrpOp ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) = ( 𝑇 ‘ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) ) )
22 fveq2 ⊢ ( ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) → ( 𝑇 ‘ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) ) = ( 𝑇 ‘ ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
23 21 22 sylan9eq ⊢ ( ( ( ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ 𝐺 ∈ GrpOp ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) ∧ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) → ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) = ( 𝑇 ‘ ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
24 23 anasss ⊢ ( ( ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ 𝐺 ∈ GrpOp ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ∧ ( ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) → ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) = ( 𝑇 ‘ ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
25 fvco3 ⊢ ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑥 ∈ ran 𝐺 ) → ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) )
26 25 ad2ant2r ⊢ ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) = ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) )
27 fvco3 ⊢ ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑦 ∈ ran 𝐺 ) → ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) = ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) )
28 27 ad2ant2rl ⊢ ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) = ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) )
29 26 28 oveq12d ⊢ ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
30 29 adantlr ⊢ ( ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ 𝐺 ∈ GrpOp ) ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
31 30 ad2ant2r ⊢ ( ( ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ 𝐺 ∈ GrpOp ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ∧ ( ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) → ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ‘ ( 𝑆 ‘ 𝑥 ) ) 𝐾 ( 𝑇 ‘ ( 𝑆 ‘ 𝑦 ) ) ) )
32 eqid ⊢ ran 𝐺 = ran 𝐺
33 32 grpocl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) → ( 𝑥 𝐺 𝑦 ) ∈ ran 𝐺 )
34 33 3expb ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( 𝑥 𝐺 𝑦 ) ∈ ran 𝐺 )
35 fvco3 ⊢ ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ( 𝑥 𝐺 𝑦 ) ∈ ran 𝐺 ) → ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝑇 ‘ ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
36 35 adantlr ⊢ ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ ( 𝑥 𝐺 𝑦 ) ∈ ran 𝐺 ) → ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝑇 ‘ ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
37 34 36 sylan2 ⊢ ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ ( 𝐺 ∈ GrpOp ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) ) → ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝑇 ‘ ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
38 37 anassrs ⊢ ( ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ 𝐺 ∈ GrpOp ) ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝑇 ‘ ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
39 38 ad2ant2r ⊢ ( ( ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ 𝐺 ∈ GrpOp ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ∧ ( ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) → ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) = ( 𝑇 ‘ ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
40 24 31 39 3eqtr4d ⊢ ( ( ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ 𝐺 ∈ GrpOp ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ∧ ( ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ∧ ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) → ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) )
41 40 expr ⊢ ( ( ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ 𝐺 ∈ GrpOp ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ∧ ( 𝑥 ∈ ran 𝐺 ∧ 𝑦 ∈ ran 𝐺 ) ) → ( ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) → ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
42 41 ralimdvva ⊢ ( ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ 𝐺 ∈ GrpOp ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) → ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
43 42 an32s ⊢ ( ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ∧ 𝐺 ∈ GrpOp ) → ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
44 43 ex ⊢ ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) → ( 𝐺 ∈ GrpOp → ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
45 44 com23 ⊢ ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ 𝑇 : ran 𝐻 ⟶ ran 𝐾 ) ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) → ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) → ( 𝐺 ∈ GrpOp → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
46 45 anasss ⊢ ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ( 𝑇 : ran 𝐻 ⟶ ran 𝐾 ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ) → ( ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) → ( 𝐺 ∈ GrpOp → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
47 46 imp ⊢ ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ( 𝑇 : ran 𝐻 ⟶ ran 𝐾 ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ) ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) → ( 𝐺 ∈ GrpOp → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
48 47 an32s ⊢ ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ∧ ( 𝑇 : ran 𝐻 ⟶ ran 𝐾 ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ) → ( 𝐺 ∈ GrpOp → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
49 48 com12 ⊢ ( 𝐺 ∈ GrpOp → ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ∧ ( 𝑇 : ran 𝐻 ⟶ ran 𝐾 ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ) → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
50 49 3ad2ant1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp ) → ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ∧ ( 𝑇 : ran 𝐻 ⟶ ran 𝐾 ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ) → ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) )
51 4 50 jcad ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp ) → ( ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ∧ ( 𝑇 : ran 𝐻 ⟶ ran 𝐾 ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ) → ( ( 𝑇 ∘ 𝑆 ) : ran 𝐺 ⟶ ran 𝐾 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
52 eqid ⊢ ran 𝐻 = ran 𝐻
53 32 52 elghomOLD ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ) → ( 𝑆 ∈ ( 𝐺 GrpOpHom 𝐻 ) ↔ ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
54 53 3adant3 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp ) → ( 𝑆 ∈ ( 𝐺 GrpOpHom 𝐻 ) ↔ ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
55 eqid ⊢ ran 𝐾 = ran 𝐾
56 52 55 elghomOLD ⊢ ( ( 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp ) → ( 𝑇 ∈ ( 𝐻 GrpOpHom 𝐾 ) ↔ ( 𝑇 : ran 𝐻 ⟶ ran 𝐾 ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ) )
57 56 3adant1 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp ) → ( 𝑇 ∈ ( 𝐻 GrpOpHom 𝐾 ) ↔ ( 𝑇 : ran 𝐻 ⟶ ran 𝐾 ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ) )
58 54 57 anbi12d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp ) → ( ( 𝑆 ∈ ( 𝐺 GrpOpHom 𝐻 ) ∧ 𝑇 ∈ ( 𝐻 GrpOpHom 𝐾 ) ) ↔ ( ( 𝑆 : ran 𝐺 ⟶ ran 𝐻 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( 𝑆 ‘ 𝑥 ) 𝐻 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑆 ‘ ( 𝑥 𝐺 𝑦 ) ) ) ∧ ( 𝑇 : ran 𝐻 ⟶ ran 𝐾 ∧ ∀ 𝑢 ∈ ran 𝐻 ∀ 𝑣 ∈ ran 𝐻 ( ( 𝑇 ‘ 𝑢 ) 𝐾 ( 𝑇 ‘ 𝑣 ) ) = ( 𝑇 ‘ ( 𝑢 𝐻 𝑣 ) ) ) ) ) )
59 32 55 elghomOLD ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐾 ∈ GrpOp ) → ( ( 𝑇 ∘ 𝑆 ) ∈ ( 𝐺 GrpOpHom 𝐾 ) ↔ ( ( 𝑇 ∘ 𝑆 ) : ran 𝐺 ⟶ ran 𝐾 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
60 59 3adant2 ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp ) → ( ( 𝑇 ∘ 𝑆 ) ∈ ( 𝐺 GrpOpHom 𝐾 ) ↔ ( ( 𝑇 ∘ 𝑆 ) : ran 𝐺 ⟶ ran 𝐾 ∧ ∀ 𝑥 ∈ ran 𝐺 ∀ 𝑦 ∈ ran 𝐺 ( ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑥 ) 𝐾 ( ( 𝑇 ∘ 𝑆 ) ‘ 𝑦 ) ) = ( ( 𝑇 ∘ 𝑆 ) ‘ ( 𝑥 𝐺 𝑦 ) ) ) ) )
61 51 58 60 3imtr4d ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp ) → ( ( 𝑆 ∈ ( 𝐺 GrpOpHom 𝐻 ) ∧ 𝑇 ∈ ( 𝐻 GrpOpHom 𝐾 ) ) → ( 𝑇 ∘ 𝑆 ) ∈ ( 𝐺 GrpOpHom 𝐾 ) ) )
62 61 imp ⊢ ( ( ( 𝐺 ∈ GrpOp ∧ 𝐻 ∈ GrpOp ∧ 𝐾 ∈ GrpOp ) ∧ ( 𝑆 ∈ ( 𝐺 GrpOpHom 𝐻 ) ∧ 𝑇 ∈ ( 𝐻 GrpOpHom 𝐾 ) ) ) → ( 𝑇 ∘ 𝑆 ) ∈ ( 𝐺 GrpOpHom 𝐾 ) )