Description: Apply a group homomorphism to a group sum, mapping version with implicit substitution. (Contributed by Mario Carneiro, 5-May-2015) (Revised by AV, 6-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | gsummhm2.b | |
|
gsummhm2.z | |
||
gsummhm2.g | |
||
gsummhm2.h | |
||
gsummhm2.a | |
||
gsummhm2.k | |
||
gsummhm2.f | |
||
gsummhm2.w | |
||
gsummhm2.1 | |
||
gsummhm2.2 | |
||
Assertion | gsummhm2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | gsummhm2.b | |
|
2 | gsummhm2.z | |
|
3 | gsummhm2.g | |
|
4 | gsummhm2.h | |
|
5 | gsummhm2.a | |
|
6 | gsummhm2.k | |
|
7 | gsummhm2.f | |
|
8 | gsummhm2.w | |
|
9 | gsummhm2.1 | |
|
10 | gsummhm2.2 | |
|
11 | 7 | fmpttd | |
12 | 1 2 3 4 5 6 11 8 | gsummhm | |
13 | eqidd | |
|
14 | eqidd | |
|
15 | 7 13 14 9 | fmptco | |
16 | 15 | oveq2d | |
17 | eqid | |
|
18 | 1 2 3 5 11 8 | gsumcl | |
19 | 10 | eleq1d | |
20 | eqid | |
|
21 | 1 20 | mhmf | |
22 | 6 21 | syl | |
23 | 17 | fmpt | |
24 | 22 23 | sylibr | |
25 | 19 24 18 | rspcdva | |
26 | 17 10 18 25 | fvmptd3 | |
27 | 12 16 26 | 3eqtr3d | |