Metamath Proof Explorer

Theorem ghmeql

Description: The equalizer of two group homomorphisms is a subgroup. (Contributed by Stefan O'Rear, 7-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Assertion ghmeql ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubGrp ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 ghmmhm ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )
2 ghmmhm ⊢ ( 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) )
3 mhmeql ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubMnd ‘ 𝑆 ) )
4 1 2 3 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubMnd ‘ 𝑆 ) )
5 fveq2 ⊢ ( 𝑦 = ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ) )
6 fveq2 ⊢ ( 𝑦 = ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ) )
7 5 6 eqeq12d ⊢ ( 𝑦 = ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐹 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ) = ( 𝐺 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ) ) )
8 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝑆 ∈ Grp )
9 8 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 𝑆 ∈ Grp )
10 9 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → 𝑆 ∈ Grp )
11 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
12 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
13 eqid ⊢ ( invg ‘ 𝑆 ) = ( invg ‘ 𝑆 )
14 12 13 grpinvcl ⊢ ( ( 𝑆 ∈ Grp ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑆 ) )
15 10 11 14 syl2anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑆 ) )
16 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
17 16 fveq2d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ( ( invg ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) = ( ( invg ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) )
18 eqid ⊢ ( invg ‘ 𝑇 ) = ( invg ‘ 𝑇 )
19 12 13 18 ghminv ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ) = ( ( invg ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
20 19 ad2ant2r ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝐹 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ) = ( ( invg ‘ 𝑇 ) ‘ ( 𝐹 ‘ 𝑥 ) ) )
21 12 13 18 ghminv ⊢ ( ( 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐺 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ) = ( ( invg ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) )
22 21 ad2ant2lr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝐺 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ) = ( ( invg ‘ 𝑇 ) ‘ ( 𝐺 ‘ 𝑥 ) ) )
23 17 20 22 3eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ( 𝐹 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ) = ( 𝐺 ‘ ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ) )
24 7 15 23 elrabd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } )
25 24 expr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) → ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } ) )
26 25 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) → ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } ) )
27 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
28 fveq2 ⊢ ( 𝑦 = 𝑥 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑥 ) )
29 27 28 eqeq12d ⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
30 29 ralrab ⊢ ( ∀ 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) → ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } ) )
31 26 30 sylibr ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ∀ 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } )
32 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
33 12 32 ghmf ⊢ ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
34 33 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
35 34 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
36 12 32 ghmf ⊢ ( 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
37 36 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
38 37 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → 𝐺 Fn ( Base ‘ 𝑆 ) )
39 fndmin ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑆 ) ∧ 𝐺 Fn ( Base ‘ 𝑆 ) ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } )
40 35 38 39 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } )
41 eleq2 ⊢ ( dom ( 𝐹 ∩ 𝐺 ) = { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } → ( ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ dom ( 𝐹 ∩ 𝐺 ) ↔ ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } ) )
42 41 raleqbi1dv ⊢ ( dom ( 𝐹 ∩ 𝐺 ) = { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } → ( ∀ 𝑥 ∈ dom ( 𝐹 ∩ 𝐺 ) ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ dom ( 𝐹 ∩ 𝐺 ) ↔ ∀ 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } ) )
43 40 42 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( ∀ 𝑥 ∈ dom ( 𝐹 ∩ 𝐺 ) ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ dom ( 𝐹 ∩ 𝐺 ) ↔ ∀ 𝑥 ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ { 𝑦 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) } ) )
44 31 43 mpbird ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ∀ 𝑥 ∈ dom ( 𝐹 ∩ 𝐺 ) ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ dom ( 𝐹 ∩ 𝐺 ) )
45 13 issubg3 ⊢ ( 𝑆 ∈ Grp → ( dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubGrp ‘ 𝑆 ) ↔ ( dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubMnd ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( 𝐹 ∩ 𝐺 ) ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ dom ( 𝐹 ∩ 𝐺 ) ) ) )
46 9 45 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → ( dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubGrp ‘ 𝑆 ) ↔ ( dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubMnd ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( 𝐹 ∩ 𝐺 ) ( ( invg ‘ 𝑆 ) ‘ 𝑥 ) ∈ dom ( 𝐹 ∩ 𝐺 ) ) ) )
47 4 44 46 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝑆 GrpHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 GrpHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubGrp ‘ 𝑆 ) )