Metamath Proof Explorer

Theorem fldcrng

Description: A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010)

Ref Expression
Assertion fldcrng ⊢ K ∈ Fld → K ∈ CRingOps

Proof

Step Hyp Ref Expression
1 eqid ⊢ 1 st ⁡ K = 1 st ⁡ K
2 eqid ⊢ 2 nd ⁡ K = 2 nd ⁡ K
3 eqid ⊢ ran ⁡ 1 st ⁡ K = ran ⁡ 1 st ⁡ K
4 eqid ⊢ GId ⁡ 1 st ⁡ K = GId ⁡ 1 st ⁡ K
5 1 2 3 4 drngoi ⊢ K ∈ DivRingOps → K ∈ RingOps ∧ 2 nd ⁡ K ↾ ran ⁡ 1 st ⁡ K ∖ GId ⁡ 1 st ⁡ K × ran ⁡ 1 st ⁡ K ∖ GId ⁡ 1 st ⁡ K ∈ GrpOp
6 5 simpld ⊢ K ∈ DivRingOps → K ∈ RingOps
7 6 anim1i ⊢ K ∈ DivRingOps ∧ K ∈ Com2 → K ∈ RingOps ∧ K ∈ Com2
8 df-fld ⊢ Fld = DivRingOps ∩ Com2
9 8 elin2 ⊢ K ∈ Fld ↔ K ∈ DivRingOps ∧ K ∈ Com2
10 iscrngo ⊢ K ∈ CRingOps ↔ K ∈ RingOps ∧ K ∈ Com2
11 7 9 10 3imtr4i ⊢ K ∈ Fld → K ∈ CRingOps