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𝑠X
Assertion resghm2b XSubGrpTranFXFSGrpHomTFSGrpHomU

Proof

Step Hyp Ref Expression
1 resghm2.u U=T𝑠X
2 ghmgrp1 FSGrpHomTSGrp
3 2 a1i XSubGrpTranFXFSGrpHomTSGrp
4 ghmgrp1 FSGrpHomUSGrp
5 4 a1i XSubGrpTranFXFSGrpHomUSGrp
6 subgsubm XSubGrpTXSubMndT
7 1 resmhm2b XSubMndTranFXFSMndHomTFSMndHomU
8 6 7 sylan XSubGrpTranFXFSMndHomTFSMndHomU
9 8 adantl SGrpXSubGrpTranFXFSMndHomTFSMndHomU
10 subgrcl XSubGrpTTGrp
11 10 adantr XSubGrpTranFXTGrp
12 ghmmhmb SGrpTGrpSGrpHomT=SMndHomT
13 11 12 sylan2 SGrpXSubGrpTranFXSGrpHomT=SMndHomT
14 13 eleq2d SGrpXSubGrpTranFXFSGrpHomTFSMndHomT
15 1 subggrp XSubGrpTUGrp
16 15 adantr XSubGrpTranFXUGrp
17 ghmmhmb SGrpUGrpSGrpHomU=SMndHomU
18 16 17 sylan2 SGrpXSubGrpTranFXSGrpHomU=SMndHomU
19 18 eleq2d SGrpXSubGrpTranFXFSGrpHomUFSMndHomU
20 9 14 19 3bitr4d SGrpXSubGrpTranFXFSGrpHomTFSGrpHomU
21 20 expcom XSubGrpTranFXSGrpFSGrpHomTFSGrpHomU
22 3 5 21 pm5.21ndd XSubGrpTranFXFSGrpHomTFSGrpHomU