Metamath Proof Explorer

Theorem mhmeql

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

Ref Expression
Assertion mhmeql ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubMnd ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
2 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
3 1 2 mhmf ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
4 3 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
5 4 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝐹 Fn ( Base ‘ 𝑆 ) )
6 1 2 mhmf ⊢ ( 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
7 6 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝐺 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
8 7 ffnd ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝐺 Fn ( Base ‘ 𝑆 ) )
9 fndmin ⊢ ( ( 𝐹 Fn ( Base ‘ 𝑆 ) ∧ 𝐺 Fn ( Base ‘ 𝑆 ) ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
10 5 8 9 syl2anc ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) = { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
11 ssrab2 ⊢ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ⊆ ( Base ‘ 𝑆 )
12 11 a1i ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ⊆ ( Base ‘ 𝑆 ) )
13 fveq2 ⊢ ( 𝑧 = ( 0g ‘ 𝑆 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) )
14 fveq2 ⊢ ( 𝑧 = ( 0g ‘ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ( 0g ‘ 𝑆 ) ) )
15 13 14 eqeq12d ⊢ ( 𝑧 = ( 0g ‘ 𝑆 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 𝐺 ‘ ( 0g ‘ 𝑆 ) ) ) )
16 mhmrcl1 ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝑆 ∈ Mnd )
17 16 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → 𝑆 ∈ Mnd )
18 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
19 1 18 mndidcl ⊢ ( 𝑆 ∈ Mnd → ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
20 17 19 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 0g ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
21 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
22 18 21 mhm0 ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
23 22 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
24 18 21 mhm0 ⊢ ( 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) → ( 𝐺 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
25 24 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐺 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
26 23 25 eqtr4d ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 𝐺 ‘ ( 0g ‘ 𝑆 ) ) )
27 15 20 26 elrabd ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( 0g ‘ 𝑆 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
28 fveq2 ⊢ ( 𝑧 = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) )
29 fveq2 ⊢ ( 𝑧 = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) )
30 28 29 eqeq12d ⊢ ( 𝑧 = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) ) )
31 17 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝑆 ∈ Mnd )
32 simplrl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
33 simprl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
34 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
35 1 34 mndcl ⊢ ( ( 𝑆 ∈ Mnd ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
36 31 32 33 35 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ ( Base ‘ 𝑆 ) )
37 simplll ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )
38 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
39 1 34 38 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
40 37 32 33 39 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
41 simpllr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) )
42 1 34 38 mhmlin ⊢ ( ( 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
43 41 32 33 42 syl3anc ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
44 simplrr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) )
45 simprr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) )
46 44 45 oveq12d ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐺 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐺 ‘ 𝑦 ) ) )
47 43 46 eqtr4d ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
48 40 47 eqtr4d ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐺 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) )
49 30 36 48 elrabd ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ ( 𝑦 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
50 49 expr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
51 50 ralrimiva ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
52 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
53 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑦 ) )
54 52 53 eqeq12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) ) )
55 54 ralrab ⊢ ( ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑦 ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
56 51 55 sylibr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ ( 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
57 56 expr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) → ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
58 57 ralrimiva ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) → ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
59 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
60 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑥 ) )
61 59 60 eqeq12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) )
62 61 ralrab ⊢ ( ∀ 𝑥 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑆 ) ( ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) → ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) )
63 58 62 sylibr ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ∀ 𝑥 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } )
64 1 18 34 issubm ⊢ ( 𝑆 ∈ Mnd → ( { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∈ ( SubMnd ‘ 𝑆 ) ↔ ( { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ⊆ ( Base ‘ 𝑆 ) ∧ ( 0g ‘ 𝑆 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∧ ∀ 𝑥 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) ) )
65 17 64 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → ( { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∈ ( SubMnd ‘ 𝑆 ) ↔ ( { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ⊆ ( Base ‘ 𝑆 ) ∧ ( 0g ‘ 𝑆 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∧ ∀ 𝑥 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∀ 𝑦 ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ) ) )
66 12 27 63 65 mpbir3and ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → { 𝑧 ∈ ( Base ‘ 𝑆 ) ∣ ( 𝐹 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) } ∈ ( SubMnd ‘ 𝑆 ) )
67 10 66 eqeltrd ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝐺 ∈ ( 𝑆 MndHom 𝑇 ) ) → dom ( 𝐹 ∩ 𝐺 ) ∈ ( SubMnd ‘ 𝑆 ) )