Metamath Proof Explorer

Theorem fldpropd

Description: If two structures have the same group components (properties), one is a field iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015)

		Ref	Expression
	Hypotheses	drngpropd.1	$⊢ φ \to B = {Base}_{K}$
		drngpropd.2	$⊢ φ \to B = {Base}_{L}$
		drngpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
		drngpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
	Assertion	fldpropd	$⊢ φ \to (K \in Field \leftrightarrow L \in Field)$

Proof

Step	Hyp	Ref	Expression
1		drngpropd.1	$⊢ φ \to B = {Base}_{K}$
2		drngpropd.2	$⊢ φ \to B = {Base}_{L}$
3		drngpropd.3	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{K} y = x +_{L} y$
4		drngpropd.4	$⊢ (φ \land (x \in B \land y \in B)) \to x \cdot_{K} y = x \cdot_{L} y$
5	1 2 3 4	drngpropd	$⊢ φ \to (K \in DivRing \leftrightarrow L \in DivRing)$
6	1 2 3 4	crngpropd	$⊢ φ \to (K \in CRing \leftrightarrow L \in CRing)$
7	5 6	anbi12d	$⊢ φ \to ((K \in DivRing \land K \in CRing) \leftrightarrow (L \in DivRing \land L \in CRing))$
8		isfld	$⊢ K \in Field \leftrightarrow (K \in DivRing \land K \in CRing)$
9		isfld	$⊢ L \in Field \leftrightarrow (L \in DivRing \land L \in CRing)$
10	7 8 9	3bitr4g	$⊢ φ \to (K \in Field \leftrightarrow L \in Field)$