Description: Expansion of the codomain of a homomorphism. (Contributed by Stefan O'Rear, 3-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | reslmhm2.u | |
|
reslmhm2.l | |
||
Assertion | reslmhm2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | reslmhm2.u | |
|
2 | reslmhm2.l | |
|
3 | eqid | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | eqid | |
|
7 | eqid | |
|
8 | eqid | |
|
9 | lmhmlmod1 | |
|
10 | 9 | 3ad2ant1 | |
11 | simp2 | |
|
12 | 1 7 | resssca | |
13 | 12 | 3ad2ant3 | |
14 | eqid | |
|
15 | 6 14 | lmhmsca | |
16 | 15 | 3ad2ant1 | |
17 | 13 16 | eqtrd | |
18 | lmghm | |
|
19 | 18 | 3ad2ant1 | |
20 | 2 | lsssubg | |
21 | 20 | 3adant1 | |
22 | 1 | resghm2 | |
23 | 19 21 22 | syl2anc | |
24 | eqid | |
|
25 | 6 8 3 4 24 | lmhmlin | |
26 | 25 | 3expb | |
27 | 26 | 3ad2antl1 | |
28 | simpl3 | |
|
29 | 1 5 | ressvsca | |
30 | 29 | oveqd | |
31 | 28 30 | syl | |
32 | 27 31 | eqtr4d | |
33 | 3 4 5 6 7 8 10 11 17 23 32 | islmhmd | |