Metamath Proof Explorer

Theorem resmhm2

Description: One direction of resmhm2b . (Contributed by Mario Carneiro, 18-Jun-2015)

Ref Expression
Hypothesis resmhm2.u 
|- U = ( T |`s X )
Assertion resmhm2 
|- ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> F e. ( S MndHom T ) )

Proof

Step Hyp Ref Expression
1 resmhm2.u 
 |-  U = ( T |`s X )
2 mhmrcl1 
 |-  ( F e. ( S MndHom U ) -> S e. Mnd )
3 submrcl 
 |-  ( X e. ( SubMnd ` T ) -> T e. Mnd )
4 2 3 anim12i 
 |-  ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> ( S e. Mnd /\ T e. Mnd ) )
5 eqid 
 |-  ( Base ` S ) = ( Base ` S )
6 eqid 
 |-  ( Base ` U ) = ( Base ` U )
7 5 6 mhmf 
 |-  ( F e. ( S MndHom U ) -> F : ( Base ` S ) --> ( Base ` U ) )
8 1 submbas 
 |-  ( X e. ( SubMnd ` T ) -> X = ( Base ` U ) )
9 eqid 
 |-  ( Base ` T ) = ( Base ` T )
10 9 submss 
 |-  ( X e. ( SubMnd ` T ) -> X C_ ( Base ` T ) )
11 8 10 eqsstrrd 
 |-  ( X e. ( SubMnd ` T ) -> ( Base ` U ) C_ ( Base ` T ) )
12 fss 
 |-  ( ( F : ( Base ` S ) --> ( Base ` U ) /\ ( Base ` U ) C_ ( Base ` T ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
13 7 11 12 syl2an 
 |-  ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
14 eqid 
 |-  ( +g ` S ) = ( +g ` S )
15 eqid 
 |-  ( +g ` U ) = ( +g ` U )
16 5 14 15 mhmlin 
 |-  ( ( F e. ( S MndHom U ) /\ x e. ( Base ` S ) /\ y e. ( Base ` S ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
17 16 3expb 
 |-  ( ( F e. ( S MndHom U ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
18 17 adantlr 
 |-  ( ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
19 eqid 
 |-  ( +g ` T ) = ( +g ` T )
20 1 19 ressplusg 
 |-  ( X e. ( SubMnd ` T ) -> ( +g ` T ) = ( +g ` U ) )
21 20 ad2antlr 
 |-  ( ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( +g ` T ) = ( +g ` U ) )
22 21 oveqd 
 |-  ( ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( ( F ` x ) ( +g ` T ) ( F ` y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
23 18 22 eqtr4d 
 |-  ( ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
24 23 ralrimivva 
 |-  ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
25 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
26 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
27 25 26 mhm0 
 |-  ( F e. ( S MndHom U ) -> ( F ` ( 0g ` S ) ) = ( 0g ` U ) )
28 27 adantr 
 |-  ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> ( F ` ( 0g ` S ) ) = ( 0g ` U ) )
29 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
30 1 29 subm0 
 |-  ( X e. ( SubMnd ` T ) -> ( 0g ` T ) = ( 0g ` U ) )
31 30 adantl 
 |-  ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> ( 0g ` T ) = ( 0g ` U ) )
32 28 31 eqtr4d 
 |-  ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
33 13 24 32 3jca 
 |-  ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` 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 ) ) /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) )
34 5 9 14 19 25 29 ismhm 
 |-  ( F e. ( S MndHom T ) <-> ( ( S e. Mnd /\ T e. Mnd ) /\ ( 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 ) ) /\ ( F ` ( 0g ` S ) ) = ( 0g ` T ) ) ) )
35 4 33 34 sylanbrc 
 |-  ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> F e. ( S MndHom T ) )