This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resghm2b

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

Ref Expression
Hypothesis resghm2.u 
|- U = ( T |`s X )
Assertion resghm2b 
|- ( ( X e. ( SubGrp ` T ) /\ ran F C_ X ) -> ( F e. ( S GrpHom T ) <-> F e. ( S GrpHom U ) ) )

Proof

Step Hyp Ref Expression
1 resghm2.u 
 |-  U = ( T |`s X )
2 ghmgrp1 
 |-  ( F e. ( S GrpHom T ) -> S e. Grp )
3 2 a1i 
 |-  ( ( X e. ( SubGrp ` T ) /\ ran F C_ X ) -> ( F e. ( S GrpHom T ) -> S e. Grp ) )
4 ghmgrp1 
 |-  ( F e. ( S GrpHom U ) -> S e. Grp )
5 4 a1i 
 |-  ( ( X e. ( SubGrp ` T ) /\ ran F C_ X ) -> ( F e. ( S GrpHom U ) -> S e. Grp ) )
6 subgsubm 
 |-  ( X e. ( SubGrp ` T ) -> X e. ( SubMnd ` T ) )
7 1 resmhm2b 
 |-  ( ( X e. ( SubMnd ` T ) /\ ran F C_ X ) -> ( F e. ( S MndHom T ) <-> F e. ( S MndHom U ) ) )
8 6 7 sylan 
 |-  ( ( X e. ( SubGrp ` T ) /\ ran F C_ X ) -> ( F e. ( S MndHom T ) <-> F e. ( S MndHom U ) ) )
9 8 adantl 
 |-  ( ( S e. Grp /\ ( X e. ( SubGrp ` T ) /\ ran F C_ X ) ) -> ( F e. ( S MndHom T ) <-> F e. ( S MndHom U ) ) )
10 subgrcl 
 |-  ( X e. ( SubGrp ` T ) -> T e. Grp )
11 10 adantr 
 |-  ( ( X e. ( SubGrp ` T ) /\ ran F C_ X ) -> T e. Grp )
12 ghmmhmb 
 |-  ( ( S e. Grp /\ T e. Grp ) -> ( S GrpHom T ) = ( S MndHom T ) )
13 11 12 sylan2 
 |-  ( ( S e. Grp /\ ( X e. ( SubGrp ` T ) /\ ran F C_ X ) ) -> ( S GrpHom T ) = ( S MndHom T ) )
14 13 eleq2d 
 |-  ( ( S e. Grp /\ ( X e. ( SubGrp ` T ) /\ ran F C_ X ) ) -> ( F e. ( S GrpHom T ) <-> F e. ( S MndHom T ) ) )
15 1 subggrp 
 |-  ( X e. ( SubGrp ` T ) -> U e. Grp )
16 15 adantr 
 |-  ( ( X e. ( SubGrp ` T ) /\ ran F C_ X ) -> U e. Grp )
17 ghmmhmb 
 |-  ( ( S e. Grp /\ U e. Grp ) -> ( S GrpHom U ) = ( S MndHom U ) )
18 16 17 sylan2 
 |-  ( ( S e. Grp /\ ( X e. ( SubGrp ` T ) /\ ran F C_ X ) ) -> ( S GrpHom U ) = ( S MndHom U ) )
19 18 eleq2d 
 |-  ( ( S e. Grp /\ ( X e. ( SubGrp ` T ) /\ ran F C_ X ) ) -> ( F e. ( S GrpHom U ) <-> F e. ( S MndHom U ) ) )
20 9 14 19 3bitr4d 
 |-  ( ( S e. Grp /\ ( X e. ( SubGrp ` T ) /\ ran F C_ X ) ) -> ( F e. ( S GrpHom T ) <-> F e. ( S GrpHom U ) ) )
21 20 expcom 
 |-  ( ( X e. ( SubGrp ` T ) /\ ran F C_ X ) -> ( S e. Grp -> ( F e. ( S GrpHom T ) <-> F e. ( S GrpHom U ) ) ) )
22 3 5 21 pm5.21ndd 
 |-  ( ( X e. ( SubGrp ` T ) /\ ran F C_ X ) -> ( F e. ( S GrpHom T ) <-> F e. ( S GrpHom U ) ) )