Metamath Proof Explorer

Theorem isfld2

Description: The predicate "is a field". (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Assertion isfld2 ( 𝐾 ∈ Fld ↔ ( 𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps ) )

Proof

Step Hyp Ref Expression
1 flddivrng ⊢ ( 𝐾 ∈ Fld → 𝐾 ∈ DivRingOps )
2 fldcrngo ⊢ ( 𝐾 ∈ Fld → 𝐾 ∈ CRingOps )
3 1 2 jca ⊢ ( 𝐾 ∈ Fld → ( 𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps ) )
4 iscrngo ⊢ ( 𝐾 ∈ CRingOps ↔ ( 𝐾 ∈ RingOps ∧ 𝐾 ∈ Com2 ) )
5 4 simprbi ⊢ ( 𝐾 ∈ CRingOps → 𝐾 ∈ Com2 )
6 elin ⊢ ( 𝐾 ∈ ( DivRingOps ∩ Com2 ) ↔ ( 𝐾 ∈ DivRingOps ∧ 𝐾 ∈ Com2 ) )
7 6 biimpri ⊢ ( ( 𝐾 ∈ DivRingOps ∧ 𝐾 ∈ Com2 ) → 𝐾 ∈ ( DivRingOps ∩ Com2 ) )
8 df-fld ⊢ Fld = ( DivRingOps ∩ Com2 )
9 7 8 eleqtrrdi ⊢ ( ( 𝐾 ∈ DivRingOps ∧ 𝐾 ∈ Com2 ) → 𝐾 ∈ Fld )
10 5 9 sylan2 ⊢ ( ( 𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps ) → 𝐾 ∈ Fld )
11 3 10 impbii ⊢ ( 𝐾 ∈ Fld ↔ ( 𝐾 ∈ DivRingOps ∧ 𝐾 ∈ CRingOps ) )