Metamath Proof Explorer

Theorem resmgmhm2

Description: One direction of resmgmhm2b . (Contributed by AV, 26-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 resmgmhm2.u 
 |-  U = ( T |`s X )
2 mgmhmrcl 
 |-  ( F e. ( S MgmHom U ) -> ( S e. Mgm /\ U e. Mgm ) )
3 2 simpld 
 |-  ( F e. ( S MgmHom U ) -> S e. Mgm )
4 submgmrcl 
 |-  ( X e. ( SubMgm ` T ) -> T e. Mgm )
5 3 4 anim12i 
 |-  ( ( F e. ( S MgmHom U ) /\ X e. ( SubMgm ` T ) ) -> ( S e. Mgm /\ T e. Mgm ) )
6 eqid 
 |-  ( Base ` S ) = ( Base ` S )
7 eqid 
 |-  ( Base ` U ) = ( Base ` U )
8 6 7 mgmhmf 
 |-  ( F e. ( S MgmHom U ) -> F : ( Base ` S ) --> ( Base ` U ) )
9 1 submgmbas 
 |-  ( X e. ( SubMgm ` T ) -> X = ( Base ` U ) )
10 eqid 
 |-  ( Base ` T ) = ( Base ` T )
11 10 submgmss 
 |-  ( X e. ( SubMgm ` T ) -> X C_ ( Base ` T ) )
12 9 11 eqsstrrd 
 |-  ( X e. ( SubMgm ` T ) -> ( Base ` U ) C_ ( Base ` T ) )
13 fss 
 |-  ( ( F : ( Base ` S ) --> ( Base ` U ) /\ ( Base ` U ) C_ ( Base ` T ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
14 8 12 13 syl2an 
 |-  ( ( F e. ( S MgmHom U ) /\ X e. ( SubMgm ` T ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
15 eqid 
 |-  ( +g ` S ) = ( +g ` S )
16 eqid 
 |-  ( +g ` U ) = ( +g ` U )
17 6 15 16 mgmhmlin 
 |-  ( ( F e. ( S MgmHom U ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
18 17 3expb 
 |-  ( ( F e. ( S MgmHom U ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
19 18 adantlr 
 |-  ( ( ( F e. ( S MgmHom U ) /\ X e. ( SubMgm ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
20 eqid 
 |-  ( +g ` T ) = ( +g ` T )
21 1 20 ressplusg 
 |-  ( X e. ( SubMgm ` T ) -> ( +g ` T ) = ( +g ` U ) )
22 21 ad2antlr 
 |-  ( ( ( F e. ( S MgmHom U ) /\ X e. ( SubMgm ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( +g ` T ) = ( +g ` U ) )
23 22 oveqd 
 |-  ( ( ( F e. ( S MgmHom U ) /\ X e. ( SubMgm ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( ( F ` x ) ( +g ` T ) ( F ` y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
24 19 23 eqtr4d 
 |-  ( ( ( F e. ( S MgmHom U ) /\ X e. ( SubMgm ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
25 24 ralrimivva 
 |-  ( ( F e. ( S MgmHom U ) /\ X e. ( SubMgm ` T ) ) -> A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
26 14 25 jca 
 |-  ( ( F e. ( S MgmHom U ) /\ X e. ( SubMgm ` T ) ) -> ( F : ( Base ` S ) --> ( Base ` T ) /\ A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) ) )
27 6 10 15 20 ismgmhm 
 |-  ( F e. ( S MgmHom T ) <-> ( ( S e. Mgm /\ T e. Mgm ) /\ ( F : ( Base ` S ) --> ( Base ` T ) /\ A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) ) ) )
28 5 26 27 sylanbrc 
 |-  ( ( F e. ( S MgmHom U ) /\ X e. ( SubMgm ` T ) ) -> F e. ( S MgmHom T ) )