Step |
Hyp |
Ref |
Expression |
1 |
|
ablpropd.1 |
|- ( ph -> B = ( Base ` K ) ) |
2 |
|
ablpropd.2 |
|- ( ph -> B = ( Base ` L ) ) |
3 |
|
ablpropd.3 |
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) ) |
4 |
1 2 3
|
grppropd |
|- ( ph -> ( K e. Grp <-> L e. Grp ) ) |
5 |
1 2 3
|
cmnpropd |
|- ( ph -> ( K e. CMnd <-> L e. CMnd ) ) |
6 |
4 5
|
anbi12d |
|- ( ph -> ( ( K e. Grp /\ K e. CMnd ) <-> ( L e. Grp /\ L e. CMnd ) ) ) |
7 |
|
isabl |
|- ( K e. Abel <-> ( K e. Grp /\ K e. CMnd ) ) |
8 |
|
isabl |
|- ( L e. Abel <-> ( L e. Grp /\ L e. CMnd ) ) |
9 |
6 7 8
|
3bitr4g |
|- ( ph -> ( K e. Abel <-> L e. Abel ) ) |