cncrng

Description: The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015) Avoid ax-mulf . (Revised by GG, 31-Mar-2025)

		Ref	Expression
	Assertion	cncrng	$⊢ ℂ_{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		mpocnfldmul	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) = \cdot_{ℂ_{fld}}$
6	5	a1i	$⊢ ⊤ \to (u \in ℂ, v \in ℂ ⟼ u v) = \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		id	$⊢ x \in ℂ \to x \in ℂ$
13	11 12	addcomd	$⊢ 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		mpomulf	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) : ℂ \times ℂ ⟶ ℂ$
19	18	fovcl	$⊢ (x \in ℂ \land y \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) y \in ℂ$
20	19	3adant1	$⊢ (⊤ \land x \in ℂ \land y \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) y \in ℂ$
21		mulass	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x y z = x y z$
22		mulcl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
23		ovmpot	$⊢ (x y \in ℂ \land z \in ℂ) \to x y (u \in ℂ, v \in ℂ ⟼ u v) z = x y z$
24	22 23	stoic3	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x y (u \in ℂ, v \in ℂ ⟼ u v) z = x y z$
25		simp1	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x \in ℂ$
26		mulcl	$⊢ (y \in ℂ \land z \in ℂ) \to y z \in ℂ$
27	26	3adant1	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to y z \in ℂ$
28		ovmpot	$⊢ (x \in ℂ \land y z \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) y z = x y z$
29	25 27 28	syl2anc	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) y z = x y z$
30	21 24 29	3eqtr4d	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x y (u \in ℂ, v \in ℂ ⟼ u v) z = x (u \in ℂ, v \in ℂ ⟼ u v) y z$
31		ovmpot	$⊢ (x \in ℂ \land y \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) y = x y$
32	31	3adant3	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) y = x y$
33	32	oveq1d	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to (x (u \in ℂ, v \in ℂ ⟼ u v) y) (u \in ℂ, v \in ℂ ⟼ u v) z = x y (u \in ℂ, v \in ℂ ⟼ u v) z$
34		ovmpot	$⊢ (y \in ℂ \land z \in ℂ) \to y (u \in ℂ, v \in ℂ ⟼ u v) z = y z$
35	34	3adant1	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to y (u \in ℂ, v \in ℂ ⟼ u v) z = y z$
36	35	oveq2d	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) (y (u \in ℂ, v \in ℂ ⟼ u v) z) = x (u \in ℂ, v \in ℂ ⟼ u v) y z$
37	30 33 36	3eqtr4d	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to (x (u \in ℂ, v \in ℂ ⟼ u v) y) (u \in ℂ, v \in ℂ ⟼ u v) z = x (u \in ℂ, v \in ℂ ⟼ u v) (y (u \in ℂ, v \in ℂ ⟼ u v) z)$
38	37	adantl	$⊢ (⊤ \land (x \in ℂ \land y \in ℂ \land z \in ℂ)) \to (x (u \in ℂ, v \in ℂ ⟼ u v) y) (u \in ℂ, v \in ℂ ⟼ u v) z = x (u \in ℂ, v \in ℂ ⟼ u v) (y (u \in ℂ, v \in ℂ ⟼ u v) z)$
39		adddi	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x (y + z) = x y + x z$
40		addcl	$⊢ (y \in ℂ \land z \in ℂ) \to y + z \in ℂ$
41	40	3adant1	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to y + z \in ℂ$
42		ovmpot	$⊢ (x \in ℂ \land y + z \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) (y + z) = x (y + z)$
43	25 41 42	syl2anc	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) (y + z) = x (y + z)$
44		ovmpot	$⊢ (x \in ℂ \land z \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) z = x z$
45	44	3adant2	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) z = x z$
46	32 45	oveq12d	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to (x (u \in ℂ, v \in ℂ ⟼ u v) y) + (x (u \in ℂ, v \in ℂ ⟼ u v) z) = x y + x z$
47	39 43 46	3eqtr4d	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) (y + z) = (x (u \in ℂ, v \in ℂ ⟼ u v) y) + (x (u \in ℂ, v \in ℂ ⟼ u v) z)$
48	47	adantl	$⊢ (⊤ \land (x \in ℂ \land y \in ℂ \land z \in ℂ)) \to x (u \in ℂ, v \in ℂ ⟼ u v) (y + z) = (x (u \in ℂ, v \in ℂ ⟼ u v) y) + (x (u \in ℂ, v \in ℂ ⟼ u v) z)$
49		adddir	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to (x + y) z = x z + y z$
50		ovmpot	$⊢ (x + y \in ℂ \land z \in ℂ) \to (x + y) (u \in ℂ, v \in ℂ ⟼ u v) z = (x + y) z$
51	7 50	stoic3	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to (x + y) (u \in ℂ, v \in ℂ ⟼ u v) z = (x + y) z$
52	45 35	oveq12d	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to (x (u \in ℂ, v \in ℂ ⟼ u v) z) + (y (u \in ℂ, v \in ℂ ⟼ u v) z) = x z + y z$
53	49 51 52	3eqtr4d	$⊢ (x \in ℂ \land y \in ℂ \land z \in ℂ) \to (x + y) (u \in ℂ, v \in ℂ ⟼ u v) z = (x (u \in ℂ, v \in ℂ ⟼ u v) z) + (y (u \in ℂ, v \in ℂ ⟼ u v) z)$
54	53	adantl	$⊢ (⊤ \land (x \in ℂ \land y \in ℂ \land z \in ℂ)) \to (x + y) (u \in ℂ, v \in ℂ ⟼ u v) z = (x (u \in ℂ, v \in ℂ ⟼ u v) z) + (y (u \in ℂ, v \in ℂ ⟼ u v) z)$
55		1cnd	$⊢ ⊤ \to 1 \in ℂ$
56		ax-1cn	$⊢ 1 \in ℂ$
57		ovmpot	$⊢ (1 \in ℂ \land x \in ℂ) \to 1 (u \in ℂ, v \in ℂ ⟼ u v) x = 1 x$
58	56 57	mpan	$⊢ x \in ℂ \to 1 (u \in ℂ, v \in ℂ ⟼ u v) x = 1 x$
59		mullid	$⊢ x \in ℂ \to 1 x = x$
60	58 59	eqtrd	$⊢ x \in ℂ \to 1 (u \in ℂ, v \in ℂ ⟼ u v) x = x$
61	60	adantl	$⊢ (⊤ \land x \in ℂ) \to 1 (u \in ℂ, v \in ℂ ⟼ u v) x = x$
62		ovmpot	$⊢ (x \in ℂ \land 1 \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) 1 = x \cdot 1$
63	56 62	mpan2	$⊢ x \in ℂ \to x (u \in ℂ, v \in ℂ ⟼ u v) 1 = x \cdot 1$
64		mulrid	$⊢ x \in ℂ \to x \cdot 1 = x$
65	63 64	eqtrd	$⊢ x \in ℂ \to x (u \in ℂ, v \in ℂ ⟼ u v) 1 = x$
66	65	adantl	$⊢ (⊤ \land x \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) 1 = x$
67		mulcom	$⊢ (x \in ℂ \land y \in ℂ) \to x y = y x$
68		ovmpot	$⊢ (y \in ℂ \land x \in ℂ) \to y (u \in ℂ, v \in ℂ ⟼ u v) x = y x$
69	68	ancoms	$⊢ (x \in ℂ \land y \in ℂ) \to y (u \in ℂ, v \in ℂ ⟼ u v) x = y x$
70	67 31 69	3eqtr4d	$⊢ (x \in ℂ \land y \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) y = y (u \in ℂ, v \in ℂ ⟼ u v) x$
71	70	3adant1	$⊢ (⊤ \land x \in ℂ \land y \in ℂ) \to x (u \in ℂ, v \in ℂ ⟼ u v) y = y (u \in ℂ, v \in ℂ ⟼ u v) x$
72	2 4 6 17 20 38 48 54 55 61 66 71	iscrngd	$⊢ ⊤ \to ℂ_{fld} \in CRing$
73	72	mptru	$⊢ ℂ_{fld} \in CRing$

Metamath Proof Explorer

Theorem cncrng

Proof