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 | |
|
Assertion | resghm2b | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | resghm2.u | |
|
2 | ghmgrp1 | |
|
3 | 2 | a1i | |
4 | ghmgrp1 | |
|
5 | 4 | a1i | |
6 | subgsubm | |
|
7 | 1 | resmhm2b | |
8 | 6 7 | sylan | |
9 | 8 | adantl | |
10 | subgrcl | |
|
11 | 10 | adantr | |
12 | ghmmhmb | |
|
13 | 11 12 | sylan2 | |
14 | 13 | eleq2d | |
15 | 1 | subggrp | |
16 | 15 | adantr | |
17 | ghmmhmb | |
|
18 | 16 17 | sylan2 | |
19 | 18 | eleq2d | |
20 | 9 14 19 | 3bitr4d | |
21 | 20 | expcom | |
22 | 3 5 21 | pm5.21ndd | |