Metamath Proof Explorer

Theorem mgmhmeql

Description: The equalizer of two magma homomorphisms is a submagma. (Contributed by AV, 27-Feb-2020)

Ref Expression
Assertion mgmhmeql ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubMgm ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
2 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
3 1 2 mgmhmf ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
4 3 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
5 4 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
6 1 2 mgmhmf ⊢ ( 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
7 6 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
8 7 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝐺 Fn ( Base ‘ 𝑆 ) )
9 fndmin ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑆 ) ∧ 𝐺 Fn ( Base ‘ 𝑆 ) ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
10 5 8 9 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
11 ssrab2 ⊢ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ⊆ ( Base ‘ 𝑆 )
12 11 a1i ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ⊆ ( Base ‘ 𝑆 ) )
13 mgmhmrcl ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → ( 𝑆 ∈ Mgm ∧ 𝑇 ∈ Mgm ) )
14 13 simpld ⊢ ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) → 𝑆 ∈ Mgm )
15 14 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → 𝑆 ∈ Mgm )
16 15 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝑆 ∈ Mgm )
17 simplrl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
18 simprl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
19 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
20 1 19 mgmcl ⊢ ( ( 𝑆 ∈ Mgm ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
21 16 17 18 20 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
22 simplrr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
23 simprr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
24 22 23 oveq12d ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
25 simplll ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) )
26 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
27 1 19 26 mgmhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
28 25 17 18 27 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
29 simpllr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) )
30 1 19 26 mgmhmlin ⊢ ( ( 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
31 29 17 18 30 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
32 24 28 31 3eqtr4d ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) )
33 fveq2 ⊢ ( 𝑧 = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) )
34 fveq2 ⊢ ( 𝑧 = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) )
35 33 34 eqeq12d ⊢ ( 𝑧 = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) )
36 35 elrab ⊢ ( ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ↔ ( ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) )
37 21 32 36 sylanbrc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
38 37 expr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
39 38 ralrimiva ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
40 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
41 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑦 ) )
42 40 41 eqeq12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) )
43 42 ralrab ⊢ ( ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
44 39 43 sylibr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
45 44 expr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) → ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
46 45 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) → ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
47 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
48 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑥 ) )
49 47 48 eqeq12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
50 49 ralrab ⊢ ( ∀ 𝑥 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) → ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
51 46 50 sylibr ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ∀ 𝑥 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
52 1 19 issubmgm ⊢ ( 𝑆 ∈ Mgm → ( { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∈ ( SubMgm ‘ 𝑆 ) ↔ ( { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ⊆ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) ) )
53 15 52 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → ( { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∈ ( SubMgm ‘ 𝑆 ) ↔ ( { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ⊆ ( Base ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) ) )
54 12 51 53 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∈ ( SubMgm ‘ 𝑆 ) )
55 10 54 eqeltrd ⊢ ( ( 𝐹 ∈ ( 𝑆 MgmHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MgmHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubMgm ‘ 𝑆 ) )