Metamath Proof Explorer

Theorem isfld2

Description: Obsolete theorem, use isfld instead. The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	isfld2	$⊢ K \in Fld \leftrightarrow (K \in DivRingOps \land K \in CRingOps)$

Proof

Step	Hyp	Ref	Expression
1		flddivrng	$⊢ K \in Fld \to K \in DivRingOps$
2		fldcrngo	$⊢ K \in Fld \to K \in CRingOps$
3	1 2	jca	$⊢ K \in Fld \to (K \in DivRingOps \land K \in CRingOps)$
4		iscrngo	$⊢ K \in CRingOps \leftrightarrow (K \in RingOps \land K \in Com2)$
5	4	simprbi	$⊢ K \in CRingOps \to K \in Com2$
6		elin	$⊢ K \in (DivRingOps \cap Com2) \leftrightarrow (K \in DivRingOps \land K \in Com2)$
7	6	biimpri	$⊢ (K \in DivRingOps \land K \in Com2) \to K \in (DivRingOps \cap Com2)$
8		df-fld	$⊢ Fld = DivRingOps \cap Com2$
9	7 8	eleqtrrdi	$⊢ (K \in DivRingOps \land K \in Com2) \to K \in Fld$
10	5 9	sylan2	$⊢ (K \in DivRingOps \land K \in CRingOps) \to K \in Fld$
11	3 10	impbii	$⊢ K \in Fld \leftrightarrow (K \in DivRingOps \land K \in CRingOps)$