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 
|- U = ( S |`s X )
Assertion resmhm 
|- ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( F |` X ) e. ( U MndHom T ) )

Proof

Step Hyp Ref Expression
1 resmhm.u 
 |-  U = ( S |`s X )
2 mhmrcl2 
 |-  ( F e. ( S MndHom T ) -> T e. Mnd )
3 1 submmnd 
 |-  ( X e. ( SubMnd ` S ) -> U e. Mnd )
4 2 3 anim12ci 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( U e. Mnd /\ T e. Mnd ) )
5 eqid 
 |-  ( Base ` S ) = ( Base ` S )
6 eqid 
 |-  ( Base ` T ) = ( Base ` T )
7 5 6 mhmf 
 |-  ( F e. ( S MndHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
8 5 submss 
 |-  ( X e. ( SubMnd ` S ) -> X C_ ( Base ` S ) )
9 fssres 
 |-  ( ( F : ( Base ` S ) --> ( Base ` T ) /\ X C_ ( Base ` S ) ) -> ( F |` X ) : X --> ( Base ` T ) )
10 7 8 9 syl2an 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( F |` X ) : X --> ( Base ` T ) )
11 8 adantl 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> X C_ ( Base ` S ) )
12 1 5 ressbas2 
 |-  ( X C_ ( Base ` S ) -> X = ( Base ` U ) )
13 11 12 syl 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> X = ( Base ` U ) )
14 13 feq2d 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( ( F |` X ) : X --> ( Base ` T ) <-> ( F |` X ) : ( Base ` U ) --> ( Base ` T ) ) )
15 10 14 mpbid 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( F |` X ) : ( Base ` U ) --> ( Base ` T ) )
16 simpll 
 |-  ( ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) /\ ( x e. X /\ y e. X ) ) -> F e. ( S MndHom T ) )
17 8 ad2antlr 
 |-  ( ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) /\ ( x e. X /\ y e. X ) ) -> X C_ ( Base ` S ) )
18 simprl 
 |-  ( ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) /\ ( x e. X /\ y e. X ) ) -> x e. X )
19 17 18 sseldd 
 |-  ( ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) /\ ( x e. X /\ y e. X ) ) -> x e. ( Base ` S ) )
20 simprr 
 |-  ( ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) /\ ( x e. X /\ y e. X ) ) -> y e. X )
21 17 20 sseldd 
 |-  ( ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) /\ ( x e. X /\ y e. X ) ) -> y e. ( Base ` S ) )
22 eqid 
 |-  ( +g ` S ) = ( +g ` S )
23 eqid 
 |-  ( +g ` T ) = ( +g ` T )
24 5 22 23 mhmlin 
 |-  ( ( F e. ( S MndHom T ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
25 16 19 21 24 syl3anc 
 |-  ( ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
26 22 submcl 
 |-  ( ( X e. ( SubMnd ` S ) /\ x e. X /\ y e. X ) -> ( x ( +g ` S ) y ) e. X )
27 26 3expb 
 |-  ( ( X e. ( SubMnd ` S ) /\ ( x e. X /\ y e. X ) ) -> ( x ( +g ` S ) y ) e. X )
28 27 adantll 
 |-  ( ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) /\ ( x e. X /\ y e. X ) ) -> ( x ( +g ` S ) y ) e. X )
29 28 fvresd 
 |-  ( ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) /\ ( x e. X /\ y e. X ) ) -> ( ( F |` X ) ` ( x ( +g ` S ) y ) ) = ( F ` ( x ( +g ` S ) y ) ) )
30 fvres 
 |-  ( x e. X -> ( ( F |` X ) ` x ) = ( F ` x ) )
31 fvres 
 |-  ( y e. X -> ( ( F |` X ) ` y ) = ( F ` y ) )
32 30 31 oveqan12d 
 |-  ( ( x e. X /\ y e. X ) -> ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
33 32 adantl 
 |-  ( ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) /\ ( x e. X /\ y e. X ) ) -> ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
34 25 29 33 3eqtr4d 
 |-  ( ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) /\ ( x e. X /\ y e. X ) ) -> ( ( F |` X ) ` ( x ( +g ` S ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) )
35 34 ralrimivva 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> A. x e. X A. y e. X ( ( F |` X ) ` ( x ( +g ` S ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) )
36 1 22 ressplusg 
 |-  ( X e. ( SubMnd ` S ) -> ( +g ` S ) = ( +g ` U ) )
37 36 adantl 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( +g ` S ) = ( +g ` U ) )
38 37 oveqd 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( x ( +g ` S ) y ) = ( x ( +g ` U ) y ) )
39 38 fveqeq2d 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( ( ( F |` X ) ` ( x ( +g ` S ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) <-> ( ( F |` X ) ` ( x ( +g ` U ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) ) )
40 13 39 raleqbidv 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( A. y e. X ( ( F |` X ) ` ( x ( +g ` S ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) <-> A. y e. ( Base ` U ) ( ( F |` X ) ` ( x ( +g ` U ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) ) )
41 13 40 raleqbidv 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( A. x e. X A. y e. X ( ( F |` X ) ` ( x ( +g ` S ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) <-> A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( ( F |` X ) ` ( x ( +g ` U ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) ) )
42 35 41 mpbid 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( ( F |` X ) ` ( x ( +g ` U ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) )
43 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
44 43 subm0cl 
 |-  ( X e. ( SubMnd ` S ) -> ( 0g ` S ) e. X )
45 44 adantl 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( 0g ` S ) e. X )
46 45 fvresd 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( ( F |` X ) ` ( 0g ` S ) ) = ( F ` ( 0g ` S ) ) )
47 1 43 subm0 
 |-  ( X e. ( SubMnd ` S ) -> ( 0g ` S ) = ( 0g ` U ) )
48 47 adantl 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( 0g ` S ) = ( 0g ` U ) )
49 48 fveq2d 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( ( F |` X ) ` ( 0g ` S ) ) = ( ( F |` X ) ` ( 0g ` U ) ) )
50 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
51 43 50 mhm0 
 |-  ( F e. ( S MndHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
52 51 adantr 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
53 46 49 52 3eqtr3d 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( ( F |` X ) ` ( 0g ` U ) ) = ( 0g ` T ) )
54 15 42 53 3jca 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( ( F |` X ) : ( Base ` U ) --> ( Base ` T ) /\ A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( ( F |` X ) ` ( x ( +g ` U ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) /\ ( ( F |` X ) ` ( 0g ` U ) ) = ( 0g ` T ) ) )
55 eqid 
 |-  ( Base ` U ) = ( Base ` U )
56 eqid 
 |-  ( +g ` U ) = ( +g ` U )
57 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
58 55 6 56 23 57 50 ismhm 
 |-  ( ( F |` X ) e. ( U MndHom T ) <-> ( ( U e. Mnd /\ T e. Mnd ) /\ ( ( F |` X ) : ( Base ` U ) --> ( Base ` T ) /\ A. x e. ( Base ` U ) A. y e. ( Base ` U ) ( ( F |` X ) ` ( x ( +g ` U ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) /\ ( ( F |` X ) ` ( 0g ` U ) ) = ( 0g ` T ) ) ) )
59 4 54 58 sylanbrc 
 |-  ( ( F e. ( S MndHom T ) /\ X e. ( SubMnd ` S ) ) -> ( F |` X ) e. ( U MndHom T ) )