Metamath Proof Explorer

Theorem fldcrngo

Description: Obsolete theorem, use fldcrngd instead. A field is a commutative ring. (Contributed by Jeff Madsen, 8-Jun-2010) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	fldcrngo	⊢ ( 𝐾 ∈ Fld → 𝐾 ∈ CRingOps )

Proof

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