Metamath Proof Explorer


Theorem ablpropd

Description: If two structures have the same group components (properties), one is an Abelian group iff the other one is. (Contributed by NM, 6-Dec-2014)

Ref Expression
Hypotheses ablpropd.1 φ B = Base K
ablpropd.2 φ B = Base L
ablpropd.3 φ x B y B x + K y = x + L y
Assertion ablpropd φ K Abel L Abel

Proof

Step Hyp Ref Expression
1 ablpropd.1 φ B = Base K
2 ablpropd.2 φ B = Base L
3 ablpropd.3 φ x B y B x + K y = x + L y
4 1 2 3 grppropd φ K Grp L Grp
5 1 2 3 cmnpropd φ K CMnd L CMnd
6 4 5 anbi12d φ K Grp K CMnd L Grp L CMnd
7 isabl K Abel K Grp K CMnd
8 isabl L Abel L Grp L CMnd
9 6 7 8 3bitr4g φ K Abel L Abel