Metamath Proof Explorer

Theorem resmgmhm

Description: Restriction of a magma homomorphism to a submagma is a homomorphism. (Contributed by AV, 26-Feb-2020)

Ref Expression
Hypothesis resmgmhm.u 
|- U = ( S |`s X )
Assertion resmgmhm 
|- ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) -> ( F |` X ) e. ( U MgmHom T ) )

Proof

Step Hyp Ref Expression
1 resmgmhm.u 
 |-  U = ( S |`s X )
2 mgmhmrcl 
 |-  ( F e. ( S MgmHom T ) -> ( S e. Mgm /\ T e. Mgm ) )
3 2 simprd 
 |-  ( F e. ( S MgmHom T ) -> T e. Mgm )
4 1 submgmmgm 
 |-  ( X e. ( SubMgm ` S ) -> U e. Mgm )
5 3 4 anim12ci 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) -> ( U e. Mgm /\ T e. Mgm ) )
6 eqid 
 |-  ( Base ` S ) = ( Base ` S )
7 eqid 
 |-  ( Base ` T ) = ( Base ` T )
8 6 7 mgmhmf 
 |-  ( F e. ( S MgmHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
9 6 submgmss 
 |-  ( X e. ( SubMgm ` S ) -> X C_ ( Base ` S ) )
10 fssres 
 |-  ( ( F : ( Base ` S ) --> ( Base ` T ) /\ X C_ ( Base ` S ) ) -> ( F |` X ) : X --> ( Base ` T ) )
11 8 9 10 syl2an 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) -> ( F |` X ) : X --> ( Base ` T ) )
12 9 adantl 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) -> X C_ ( Base ` S ) )
13 1 6 ressbas2 
 |-  ( X C_ ( Base ` S ) -> X = ( Base ` U ) )
14 12 13 syl 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) -> X = ( Base ` U ) )
15 14 feq2d 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) -> ( ( F |` X ) : X --> ( Base ` T ) <-> ( F |` X ) : ( Base ` U ) --> ( Base ` T ) ) )
16 11 15 mpbid 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) -> ( F |` X ) : ( Base ` U ) --> ( Base ` T ) )
17 simpll 
 |-  ( ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) /\ ( x e. X /\ y e. X ) ) -> F e. ( S MgmHom T ) )
18 9 ad2antlr 
 |-  ( ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) /\ ( x e. X /\ y e. X ) ) -> X C_ ( Base ` S ) )
19 simprl 
 |-  ( ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) /\ ( x e. X /\ y e. X ) ) -> x e. X )
20 18 19 sseldd 
 |-  ( ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) /\ ( x e. X /\ y e. X ) ) -> x e. ( Base ` S ) )
21 simprr 
 |-  ( ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) /\ ( x e. X /\ y e. X ) ) -> y e. X )
22 18 21 sseldd 
 |-  ( ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) /\ ( x e. X /\ y e. X ) ) -> y e. ( Base ` S ) )
23 eqid 
 |-  ( +g ` S ) = ( +g ` S )
24 eqid 
 |-  ( +g ` T ) = ( +g ` T )
25 6 23 24 mgmhmlin 
 |-  ( ( F e. ( S MgmHom T ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
26 17 20 22 25 syl3anc 
 |-  ( ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
27 23 submgmcl 
 |-  ( ( X e. ( SubMgm ` S ) /\ x e. X /\ y e. X ) -> ( x ( +g ` S ) y ) e. X )
28 27 3expb 
 |-  ( ( X e. ( SubMgm ` S ) /\ ( x e. X /\ y e. X ) ) -> ( x ( +g ` S ) y ) e. X )
29 28 adantll 
 |-  ( ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) /\ ( x e. X /\ y e. X ) ) -> ( x ( +g ` S ) y ) e. X )
30 fvres 
 |-  ( ( x ( +g ` S ) y ) e. X -> ( ( F |` X ) ` ( x ( +g ` S ) y ) ) = ( F ` ( x ( +g ` S ) y ) ) )
31 29 30 syl 
 |-  ( ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) /\ ( x e. X /\ y e. X ) ) -> ( ( F |` X ) ` ( x ( +g ` S ) y ) ) = ( F ` ( x ( +g ` S ) y ) ) )
32 fvres 
 |-  ( x e. X -> ( ( F |` X ) ` x ) = ( F ` x ) )
33 fvres 
 |-  ( y e. X -> ( ( F |` X ) ` y ) = ( F ` y ) )
34 32 33 oveqan12d 
 |-  ( ( x e. X /\ y e. X ) -> ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
35 34 adantl 
 |-  ( ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) /\ ( x e. X /\ y e. X ) ) -> ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
36 26 31 35 3eqtr4d 
 |-  ( ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) /\ ( x e. X /\ y e. X ) ) -> ( ( F |` X ) ` ( x ( +g ` S ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) )
37 36 ralrimivva 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) -> A. x e. X A. y e. X ( ( F |` X ) ` ( x ( +g ` S ) y ) ) = ( ( ( F |` X ) ` x ) ( +g ` T ) ( ( F |` X ) ` y ) ) )
38 1 23 ressplusg 
 |-  ( X e. ( SubMgm ` S ) -> ( +g ` S ) = ( +g ` U ) )
39 38 adantl 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) -> ( +g ` S ) = ( +g ` U ) )
40 39 oveqd 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) -> ( x ( +g ` S ) y ) = ( x ( +g ` U ) y ) )
41 40 fveqeq2d 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` 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 ) ) ) )
42 14 41 raleqbidv 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` 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 ) ) ) )
43 14 42 raleqbidv 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` 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 ) ) ) )
44 37 43 mpbid 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` 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 ) ) )
45 16 44 jca 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` 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 ) ) ) )
46 eqid 
 |-  ( Base ` U ) = ( Base ` U )
47 eqid 
 |-  ( +g ` U ) = ( +g ` U )
48 46 7 47 24 ismgmhm 
 |-  ( ( F |` X ) e. ( U MgmHom T ) <-> ( ( U e. Mgm /\ T e. Mgm ) /\ ( ( 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 ) ) ) ) )
49 5 45 48 sylanbrc 
 |-  ( ( F e. ( S MgmHom T ) /\ X e. ( SubMgm ` S ) ) -> ( F |` X ) e. ( U MgmHom T ) )