cncrngOLD

Description: Obsolete version of cncrng as of 30-Apr-2025. (Contributed by Mario Carneiro, 8-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	cncrngOLD	$⊢ ℂ_{fld} \in CRing$

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
2	1	a1i	$⊢ ⊤ \to ℂ = {Base}_{ℂ_{fld}}$
3		cnfldadd	$⊢ + = +_{ℂ_{fld}}$
4	3	a1i	$⊢ ⊤ \to + = +_{ℂ_{fld}}$
5		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
6	5	a1i	$⊢ ⊤ \to \times = \cdot_{ℂ_{fld}}$
7		addcl	$⊢ (x \in ℂ \land y \in ℂ) \to x + y \in ℂ$
8		addass	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x + y + z = x + y + z$
9		0cn	$⊢ 0 \in ℂ$
10		addlid	$⊢ x \in ℂ \to 0 + x = x$
11		negcl	$⊢ x \in ℂ \to - x \in ℂ$
12		addcom	$⊢ (- x \in ℂ \land x \in ℂ) \to - x + x = x + (- x)$
13	11 12	mpancom	$⊢ x \in ℂ \to - x + x = x + (- x)$
14		negid	$⊢ x \in ℂ \to x + (- x) = 0$
15	13 14	eqtrd	$⊢ x \in ℂ \to - x + x = 0$
16	1 3 7 8 9 10 11 15	isgrpi	$⊢ ℂ_{fld} \in Grp$
17	16	a1i	$⊢ ⊤ \to ℂ_{fld} \in Grp$
18		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
19	18	3adant1	$⊢ (⊤ \land x \in ℂ \land y \in ℂ) \to x y \in ℂ$
20		mulass	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x y z = x y z$
21	20	adantl	$⊢ (⊤ \land (x \in ℂ \land y \in ℂ \land z \in ℂ)) \to x y z = x y z$
22		adddi	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x (y + z) = x y + x z$
23	22	adantl	$⊢ (⊤ \land (x \in ℂ \land y \in ℂ \land z \in ℂ)) \to x (y + z) = x y + x z$
24		adddir	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to (x + y) z = x z + y z$
25	24	adantl	$⊢ (⊤ \land (x \in ℂ \land y \in ℂ \land z \in ℂ)) \to (x + y) z = x z + y z$
26		1cnd	$⊢ ⊤ \to 1 \in ℂ$
27		mullid	$⊢ x \in ℂ \to 1 x = x$
28	27	adantl	$⊢ (⊤ \land x \in ℂ) \to 1 x = x$
29		mulrid	$⊢ x \in ℂ \to x \cdot 1 = x$
30	29	adantl	$⊢ (⊤ \land x \in ℂ) \to x \cdot 1 = x$
31		mulcom	$⊢ (x \in ℂ \land y \in ℂ) \to x y = y x$
32	31	3adant1	$⊢ (⊤ \land x \in ℂ \land y \in ℂ) \to x y = y x$
33	2 4 6 17 19 21 23 25 26 28 30 32	iscrngd	$⊢ ⊤ \to ℂ_{fld} \in CRing$
34	33	mptru	$⊢ ℂ_{fld} \in CRing$

Metamath Proof Explorer

Theorem cncrngOLD

Proof