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	$⊢ φ \to B = {Base}_{K}$
		ablpropd.2	$⊢ φ \to B = {Base}_{L}$
		ablpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
	Assertion	ablpropd	$⊢ φ \to (K \in Abel \leftrightarrow L \in Abel)$

Proof

Step	Hyp	Ref	Expression
1		ablpropd.1	$⊢ φ \to B = {Base}_{K}$
2		ablpropd.2	$⊢ φ \to B = {Base}_{L}$
3		ablpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
4	1 2 3	grppropd	$⊢ φ \to (K \in Grp \leftrightarrow L \in Grp)$
5	1 2 3	cmnpropd	$⊢ φ \to (K \in CMnd \leftrightarrow L \in CMnd)$
6	4 5	anbi12d	$⊢ φ \to ((K \in Grp \land K \in CMnd) \leftrightarrow (L \in Grp \land L \in CMnd))$
7		isabl	$⊢ K \in Abel \leftrightarrow (K \in Grp \land K \in CMnd)$
8		isabl	$⊢ L \in Abel \leftrightarrow (L \in Grp \land L \in CMnd)$
9	6 7 8	3bitr4g	$⊢ φ \to (K \in Abel \leftrightarrow L \in Abel)$