Description: Group homomorphism depends only on the group attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ghmpropd.a | |
|
ghmpropd.b | |
||
ghmpropd.c | |
||
ghmpropd.d | |
||
ghmpropd.e | |
||
ghmpropd.f | |
||
Assertion | ghmpropd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ghmpropd.a | |
|
2 | ghmpropd.b | |
|
3 | ghmpropd.c | |
|
4 | ghmpropd.d | |
|
5 | ghmpropd.e | |
|
6 | ghmpropd.f | |
|
7 | 1 3 5 | grppropd | |
8 | 2 4 6 | grppropd | |
9 | 7 8 | anbi12d | |
10 | 1 2 3 4 5 6 | mhmpropd | |
11 | 10 | eleq2d | |
12 | 9 11 | anbi12d | |
13 | ghmgrp1 | |
|
14 | ghmgrp2 | |
|
15 | 13 14 | jca | |
16 | ghmmhmb | |
|
17 | 16 | eleq2d | |
18 | 15 17 | biadanii | |
19 | ghmgrp1 | |
|
20 | ghmgrp2 | |
|
21 | 19 20 | jca | |
22 | ghmmhmb | |
|
23 | 22 | eleq2d | |
24 | 21 23 | biadanii | |
25 | 12 18 24 | 3bitr4g | |
26 | 25 | eqrdv | |