fldcrngo

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

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

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 \in DivRingOps \to (K \in RingOps \land {2^{nd} (K) ↾}_{((ran 1^{st} (K) ∖ \{GId (1^{st} (K))\}) \times (ran 1^{st} (K) ∖ \{GId (1^{st} (K))\}))} \in GrpOp)$
6	5	simpld	$⊢ K \in DivRingOps \to K \in RingOps$
7	6	anim1i	$⊢ (K \in DivRingOps \land K \in Com2) \to (K \in RingOps \land K \in Com2)$
8		df-fld	$⊢ Fld = DivRingOps \cap Com2$
9	8	elin2	$⊢ K \in Fld \leftrightarrow (K \in DivRingOps \land K \in Com2)$
10		iscrngo	$⊢ K \in CRingOps \leftrightarrow (K \in RingOps \land K \in Com2)$
11	7 9 10	3imtr4i	$⊢ K \in Fld \to K \in CRingOps$

Metamath Proof Explorer