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 ) )