Metamath Proof Explorer

Theorem resmhm

Description: Restriction of a monoid homomorphism to a submonoid is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015)

Ref Expression
Hypothesis resmhm.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑋 )
Assertion resmhm ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑈 MndHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 resmhm.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑋 )
2 mhmrcl2 ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝑇 ∈ Mnd )
3 1 submmnd ⊢ ( 𝑋 ∈ ( SubMnd ‘ 𝑆 ) → 𝑈 ∈ Mnd )
4 2 3 anim12ci ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( 𝑈 ∈ Mnd ∧ 𝑇 ∈ Mnd ) )
5 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
6 eqid ⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
7 5 6 mhmf ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) )
8 5 submss ⊢ ( 𝑋 ∈ ( SubMnd ‘ 𝑆 ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
9 fssres ⊢ ( ( 𝐹 : ( Base ‘ 𝑆 ) ⟶ ( Base ‘ 𝑇 ) ∧ 𝑋 ⊆ ( Base ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) : 𝑋 ⟶ ( Base ‘ 𝑇 ) )
10 7 8 9 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) : 𝑋 ⟶ ( Base ‘ 𝑇 ) )
11 8 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
12 1 5 ressbas2 ⊢ ( 𝑋 ⊆ ( Base ‘ 𝑆 ) → 𝑋 = ( Base ‘ 𝑈 ) )
13 11 12 syl ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → 𝑋 = ( Base ‘ 𝑈 ) )
14 13 feq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( ( 𝐹 ↾ 𝑋 ) : 𝑋 ⟶ ( Base ‘ 𝑇 ) ↔ ( 𝐹 ↾ 𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ) )
15 10 14 mpbid ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) )
16 simpll ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) )
17 8 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑋 ⊆ ( Base ‘ 𝑆 ) )
18 simprl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
19 17 18 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
20 simprr ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
21 17 20 sseldd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
22 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
23 eqid ⊢ ( +g ‘ 𝑇 ) = ( +g ‘ 𝑇 )
24 5 22 23 mhmlin ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑥 ∈ ( Base ‘ 𝑆 ) ∧ 𝑦 ∈ ( Base ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
25 16 19 21 24 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
26 22 submcl ⊢ ( ( 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ 𝑋 )
27 26 3expb ⊢ ( ( 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ 𝑋 )
28 27 adantll ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ∈ 𝑋 )
29 28 fvresd ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) )
30 fvres ⊢ ( 𝑥 ∈ 𝑋 → ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
31 fvres ⊢ ( 𝑦 ∈ 𝑋 → ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) = ( 𝐹 ‘ 𝑦 ) )
32 30 31 oveqan12d ⊢ ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
33 32 adantl ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( 𝐹 ‘ 𝑦 ) ) )
34 25 29 33 3eqtr4d ⊢ ( ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) )
35 34 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) )
36 1 22 ressplusg ⊢ ( 𝑋 ∈ ( SubMnd ‘ 𝑆 ) → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑈 ) )
37 36 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( +g ‘ 𝑆 ) = ( +g ‘ 𝑈 ) )
38 37 oveqd ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) )
39 38 fveqeq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ↔ ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) )
40 13 39 raleqbidv ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) )
41 13 40 raleqbidv ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ) )
42 35 41 mpbid ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) )
43 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
44 43 subm0cl ⊢ ( 𝑋 ∈ ( SubMnd ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) ∈ 𝑋 )
45 44 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( 0g ‘ 𝑆 ) ∈ 𝑋 )
46 45 fvresd ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 0g ‘ 𝑆 ) ) = ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) )
47 1 43 subm0 ⊢ ( 𝑋 ∈ ( SubMnd ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
48 47 adantl ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
49 48 fveq2d ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 0g ‘ 𝑆 ) ) = ( ( 𝐹 ↾ 𝑋 ) ‘ ( 0g ‘ 𝑈 ) ) )
50 eqid ⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
51 43 50 mhm0 ⊢ ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
52 51 adantr ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( 𝐹 ‘ ( 0g ‘ 𝑆 ) ) = ( 0g ‘ 𝑇 ) )
53 46 49 52 3eqtr3d ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( ( 𝐹 ↾ 𝑋 ) ‘ ( 0g ‘ 𝑈 ) ) = ( 0g ‘ 𝑇 ) )
54 15 42 53 3jca ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( ( 𝐹 ↾ 𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ∧ ( ( 𝐹 ↾ 𝑋 ) ‘ ( 0g ‘ 𝑈 ) ) = ( 0g ‘ 𝑇 ) ) )
55 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
56 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
57 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
58 55 6 56 23 57 50 ismhm ⊢ ( ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑈 MndHom 𝑇 ) ↔ ( ( 𝑈 ∈ Mnd ∧ 𝑇 ∈ Mnd ) ∧ ( ( 𝐹 ↾ 𝑋 ) : ( Base ‘ 𝑈 ) ⟶ ( Base ‘ 𝑇 ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑈 ) ∀ 𝑦 ∈ ( Base ‘ 𝑈 ) ( ( 𝐹 ↾ 𝑋 ) ‘ ( 𝑥 ( +g ‘ 𝑈 ) 𝑦 ) ) = ( ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑥 ) ( +g ‘ 𝑇 ) ( ( 𝐹 ↾ 𝑋 ) ‘ 𝑦 ) ) ∧ ( ( 𝐹 ↾ 𝑋 ) ‘ ( 0g ‘ 𝑈 ) ) = ( 0g ‘ 𝑇 ) ) ) )
59 4 54 58 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑆 MndHom 𝑇 ) ∧ 𝑋 ∈ ( SubMnd ‘ 𝑆 ) ) → ( 𝐹 ↾ 𝑋 ) ∈ ( 𝑈 MndHom 𝑇 ) )