Theorem fldcrngo

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

	Ref	Expression
Assertion	fldcrngo	$$⊢K\in \mathrm{Fld}\to K\in \mathrm{CRingOps}$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢1^{st}\left(K\right)=1^{st}\left(K\right)$$
2		eqid	$$⊢2^{nd}\left(K\right)=2^{nd}\left(K\right)$$
3		eqid	$$⊢\mathrm{ran}{1}^{st}\left(K\right)=\mathrm{ran}{1}^{st}\left(K\right)$$
4		eqid	$$⊢\mathrm{GId}\left(1^{st}\left(K\right)\right)=\mathrm{GId}\left(1^{st}\left(K\right)\right)$$
5	1 2 3 4	drngoi	$$⊢K\in \mathrm{DivRingOps}\to \left(K\in \mathrm{RingOps}\wedge {2^{nd}\left(K\right)\upharpoonright }_{\left(\left(\mathrm{ran}{1}^{st}\left(K\right)\setminus \left\{\mathrm{GId}\left(1^{st}\left(K\right)\right)\right\}\right)\times \left(\mathrm{ran}{1}^{st}\left(K\right)\setminus \left\{\mathrm{GId}\left(1^{st}\left(K\right)\right)\right\}\right)\right)}\in \mathrm{GrpOp}\right)$$
6	5	simpld	$$⊢K\in \mathrm{DivRingOps}\to K\in \mathrm{RingOps}$$
7	6	anim1i	$$⊢\left(K\in \mathrm{DivRingOps}\wedge K\in \mathrm{Com2}\right)\to \left(K\in \mathrm{RingOps}\wedge K\in \mathrm{Com2}\right)$$
8		df-fld	$$⊢\mathrm{Fld}=\mathrm{DivRingOps}\cap \mathrm{Com2}$$
9	8	elin2	$$⊢K\in \mathrm{Fld}\leftrightarrow \left(K\in \mathrm{DivRingOps}\wedge K\in \mathrm{Com2}\right)$$
10		iscrngo	$$⊢K\in \mathrm{CRingOps}\leftrightarrow \left(K\in \mathrm{RingOps}\wedge K\in \mathrm{Com2}\right)$$
11	7 9 10	3imtr4i	$$⊢K\in \mathrm{Fld}\to K\in \mathrm{CRingOps}$$