Theorem cncrng

Description: The complex numbers form a commutative ring. (Contributed by Mario Carneiro, 8-Jan-2015)

	Ref	Expression
Assertion	cncrng	⊢ ℂfld ∈ CRing

Proof

Step	Hyp	Ref	Expression
1		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
2	1	a1i	⊢ ( ⊤ → ℂ = ( Base ‘ ℂfld ) )
3		cnfldadd	⊢ + = ( +g ‘ ℂfld )
4	3	a1i	⊢ ( ⊤ → + = ( +g ‘ ℂfld ) )
5		cnfldmul	⊢ · = ( .r ‘ ℂfld )
6	5	a1i	⊢ ( ⊤ → · = ( .r ‘ ℂfld ) )
7		addcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
8		addass	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
9		0cn	⊢ 0 ∈ ℂ
10		addid2	⊢ ( 𝑥 ∈ ℂ → ( 0 + 𝑥 ) = 𝑥 )
11		negcl	⊢ ( 𝑥 ∈ ℂ → - 𝑥 ∈ ℂ )
12		addcom	⊢ ( ( - 𝑥 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( - 𝑥 + 𝑥 ) = ( 𝑥 + - 𝑥 ) )
13	11 12	mpancom	⊢ ( 𝑥 ∈ ℂ → ( - 𝑥 + 𝑥 ) = ( 𝑥 + - 𝑥 ) )
14		negid	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 + - 𝑥 ) = 0 )
15	13 14	eqtrd	⊢ ( 𝑥 ∈ ℂ → ( - 𝑥 + 𝑥 ) = 0 )
16	1 3 7 8 9 10 11 15	isgrpi	⊢ ℂfld ∈ Grp
17	16	a1i	⊢ ( ⊤ → ℂfld ∈ Grp )
18		mulcl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
19	18	3adant1	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
20		mulass	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
21	20	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
22		adddi	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
23	22	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
24		adddir	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
25	24	adantl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
26		1cnd	⊢ ( ⊤ → 1 ∈ ℂ )
27		mulid2	⊢ ( 𝑥 ∈ ℂ → ( 1 · 𝑥 ) = 𝑥 )
28	27	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 1 · 𝑥 ) = 𝑥 )
29		mulid1	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 1 ) = 𝑥 )
30	29	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 · 1 ) = 𝑥 )
31		mulcom	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
32	31	3adant1	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
33	2 4 6 17 19 21 23 25 26 28 30 32	iscrngd	⊢ ( ⊤ → ℂfld ∈ CRing )
34	33	mptru	⊢ ℂfld ∈ CRing