Metamath Proof Explorer

Theorem resmhm2b

Description: Restriction of the codomain of a homomorphism. (Contributed by Mario Carneiro, 18-Jun-2015)

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

Proof

Step Hyp Ref Expression
1 resmhm2.u 
 |-  U = ( T |`s X )
2 mhmrcl1 
 |-  ( F e. ( S MndHom T ) -> S e. Mnd )
3 2 adantl 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> S e. Mnd )
4 1 submmnd 
 |-  ( X e. ( SubMnd ` T ) -> U e. Mnd )
5 4 ad2antrr 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> U e. Mnd )
6 eqid 
 |-  ( Base ` S ) = ( Base ` S )
7 eqid 
 |-  ( Base ` T ) = ( Base ` T )
8 6 7 mhmf 
 |-  ( F e. ( S MndHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
9 8 adantl 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
10 9 ffnd 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> F Fn ( Base ` S ) )
11 simplr 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> ran F C_ X )
12 df-f 
 |-  ( F : ( Base ` S ) --> X <-> ( F Fn ( Base ` S ) /\ ran F C_ X ) )
13 10 11 12 sylanbrc 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> F : ( Base ` S ) --> X )
14 1 submbas 
 |-  ( X e. ( SubMnd ` T ) -> X = ( Base ` U ) )
15 14 ad2antrr 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> X = ( Base ` U ) )
16 15 feq3d 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> ( F : ( Base ` S ) --> X <-> F : ( Base ` S ) --> ( Base ` U ) ) )
17 13 16 mpbid 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> F : ( Base ` S ) --> ( Base ` U ) )
18 eqid 
 |-  ( +g ` S ) = ( +g ` S )
19 eqid 
 |-  ( +g ` T ) = ( +g ` T )
20 6 18 19 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 ) ) )
21 20 3expb 
 |-  ( ( F e. ( S MndHom T ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
22 21 adantll 
 |-  ( ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
23 1 19 ressplusg 
 |-  ( X e. ( SubMnd ` T ) -> ( +g ` T ) = ( +g ` U ) )
24 23 ad3antrrr 
 |-  ( ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( +g ` T ) = ( +g ` U ) )
25 24 oveqd 
 |-  ( ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( ( F ` x ) ( +g ` T ) ( F ` y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
26 22 25 eqtrd 
 |-  ( ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
27 26 ralrimivva 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
28 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
29 eqid 
 |-  ( 0g ` T ) = ( 0g ` T )
30 28 29 mhm0 
 |-  ( F e. ( S MndHom T ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
31 30 adantl 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> ( F ` ( 0g ` S ) ) = ( 0g ` T ) )
32 1 29 subm0 
 |-  ( X e. ( SubMnd ` T ) -> ( 0g ` T ) = ( 0g ` U ) )
33 32 ad2antrr 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> ( 0g ` T ) = ( 0g ` U ) )
34 31 33 eqtrd 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> ( F ` ( 0g ` S ) ) = ( 0g ` U ) )
35 17 27 34 3jca 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> ( F : ( Base ` S ) --> ( Base ` U ) /\ A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) /\ ( F ` ( 0g ` S ) ) = ( 0g ` U ) ) )
36 eqid 
 |-  ( Base ` U ) = ( Base ` U )
37 eqid 
 |-  ( +g ` U ) = ( +g ` U )
38 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
39 6 36 18 37 28 38 ismhm 
 |-  ( F e. ( S MndHom U ) <-> ( ( S e. Mnd /\ U e. Mnd ) /\ ( F : ( Base ` S ) --> ( Base ` U ) /\ A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) /\ ( F ` ( 0g ` S ) ) = ( 0g ` U ) ) ) )
40 3 5 35 39 syl21anbrc 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom T ) ) -> F e. ( S MndHom U ) )
41 1 resmhm2 
 |-  ( ( F e. ( S MndHom U ) /\ X e. ( SubMnd ` T ) ) -> F e. ( S MndHom T ) )
42 41 ancoms 
 |-  ( ( X e. ( SubMnd ` T ) /\ F e. ( S MndHom U ) ) -> F e. ( S MndHom T ) )
43 42 adantlr 
 |-  ( ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) /\ F e. ( S MndHom U ) ) -> F e. ( S MndHom T ) )
44 40 43 impbida 
 |-  ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) -> ( F e. ( S MndHom T ) <-> F e. ( S MndHom U ) ) )