Metamath Proof Explorer

Theorem resmgmhm2b

Description: Restriction of the codomain of a homomorphism. (Contributed by AV, 26-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 resmgmhm2.u 
 |-  U = ( T |`s X )
2 mgmhmrcl 
 |-  ( F e. ( S MgmHom T ) -> ( S e. Mgm /\ T e. Mgm ) )
3 2 simpld 
 |-  ( F e. ( S MgmHom T ) -> S e. Mgm )
4 3 adantl 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) -> S e. Mgm )
5 1 submgmmgm 
 |-  ( X e. ( SubMgm ` T ) -> U e. Mgm )
6 5 ad2antrr 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) -> U e. Mgm )
7 4 6 jca 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) -> ( S e. Mgm /\ U e. Mgm ) )
8 eqid 
 |-  ( Base ` S ) = ( Base ` S )
9 eqid 
 |-  ( Base ` T ) = ( Base ` T )
10 8 9 mgmhmf 
 |-  ( F e. ( S MgmHom T ) -> F : ( Base ` S ) --> ( Base ` T ) )
11 10 adantl 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) -> F : ( Base ` S ) --> ( Base ` T ) )
12 11 ffnd 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) -> F Fn ( Base ` S ) )
13 simplr 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) -> ran F C_ X )
14 df-f 
 |-  ( F : ( Base ` S ) --> X <-> ( F Fn ( Base ` S ) /\ ran F C_ X ) )
15 12 13 14 sylanbrc 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) -> F : ( Base ` S ) --> X )
16 1 submgmbas 
 |-  ( X e. ( SubMgm ` T ) -> X = ( Base ` U ) )
17 16 ad2antrr 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) -> X = ( Base ` U ) )
18 17 feq3d 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) -> ( F : ( Base ` S ) --> X <-> F : ( Base ` S ) --> ( Base ` U ) ) )
19 15 18 mpbid 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) -> F : ( Base ` S ) --> ( Base ` U ) )
20 eqid 
 |-  ( +g ` S ) = ( +g ` S )
21 eqid 
 |-  ( +g ` T ) = ( +g ` T )
22 8 20 21 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 ) ) )
23 22 3expb 
 |-  ( ( F e. ( S MgmHom T ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
24 23 adantll 
 |-  ( ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` T ) ( F ` y ) ) )
25 1 21 ressplusg 
 |-  ( X e. ( SubMgm ` T ) -> ( +g ` T ) = ( +g ` U ) )
26 25 ad3antrrr 
 |-  ( ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( +g ` T ) = ( +g ` U ) )
27 26 oveqd 
 |-  ( ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( ( F ` x ) ( +g ` T ) ( F ` y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
28 24 27 eqtrd 
 |-  ( ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) /\ ( x e. ( Base ` S ) /\ y e. ( Base ` S ) ) ) -> ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
29 28 ralrimivva 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) -> A. x e. ( Base ` S ) A. y e. ( Base ` S ) ( F ` ( x ( +g ` S ) y ) ) = ( ( F ` x ) ( +g ` U ) ( F ` y ) ) )
30 19 29 jca 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom 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 ) ) ) )
31 eqid 
 |-  ( Base ` U ) = ( Base ` U )
32 eqid 
 |-  ( +g ` U ) = ( +g ` U )
33 8 31 20 32 ismgmhm 
 |-  ( F e. ( S MgmHom U ) <-> ( ( S e. Mgm /\ U e. Mgm ) /\ ( 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 ) ) ) ) )
34 7 30 33 sylanbrc 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom T ) ) -> F e. ( S MgmHom U ) )
35 1 resmgmhm2 
 |-  ( ( F e. ( S MgmHom U ) /\ X e. ( SubMgm ` T ) ) -> F e. ( S MgmHom T ) )
36 35 ancoms 
 |-  ( ( X e. ( SubMgm ` T ) /\ F e. ( S MgmHom U ) ) -> F e. ( S MgmHom T ) )
37 36 adantlr 
 |-  ( ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) /\ F e. ( S MgmHom U ) ) -> F e. ( S MgmHom T ) )
38 34 37 impbida 
 |-  ( ( X e. ( SubMgm ` T ) /\ ran F C_ X ) -> ( F e. ( S MgmHom T ) <-> F e. ( S MgmHom U ) ) )