Theorem cnsrng

Description: The complex numbers form a *-ring. (Contributed by Mario Carneiro, 6-Oct-2015)

	Ref	Expression
Assertion	cnsrng	⊢ ℂfld ∈ *-Ring

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		cnfldcj	⊢ ∗ = ( *𝑟 ‘ ℂfld )
8	7	a1i	⊢ ( ⊤ → ∗ = ( *𝑟 ‘ ℂfld ) )
9		cnring	⊢ ℂfld ∈ Ring
10	9	a1i	⊢ ( ⊤ → ℂfld ∈ Ring )
11		cjcl	⊢ ( 𝑥 ∈ ℂ → ( ∗ ‘ 𝑥 ) ∈ ℂ )
12	11	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ∗ ‘ 𝑥 ) ∈ ℂ )
13		cjadd	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ∗ ‘ ( 𝑥 + 𝑦 ) ) = ( ( ∗ ‘ 𝑥 ) + ( ∗ ‘ 𝑦 ) ) )
14	13	3adant1	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ∗ ‘ ( 𝑥 + 𝑦 ) ) = ( ( ∗ ‘ 𝑥 ) + ( ∗ ‘ 𝑦 ) ) )
15		mulcom	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
16	15	fveq2d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ∗ ‘ ( 𝑥 · 𝑦 ) ) = ( ∗ ‘ ( 𝑦 · 𝑥 ) ) )
17		cjmul	⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ∗ ‘ ( 𝑦 · 𝑥 ) ) = ( ( ∗ ‘ 𝑦 ) · ( ∗ ‘ 𝑥 ) ) )
18	17	ancoms	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ∗ ‘ ( 𝑦 · 𝑥 ) ) = ( ( ∗ ‘ 𝑦 ) · ( ∗ ‘ 𝑥 ) ) )
19	16 18	eqtrd	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ∗ ‘ ( 𝑥 · 𝑦 ) ) = ( ( ∗ ‘ 𝑦 ) · ( ∗ ‘ 𝑥 ) ) )
20	19	3adant1	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ∗ ‘ ( 𝑥 · 𝑦 ) ) = ( ( ∗ ‘ 𝑦 ) · ( ∗ ‘ 𝑥 ) ) )
21		cjcj	⊢ ( 𝑥 ∈ ℂ → ( ∗ ‘ ( ∗ ‘ 𝑥 ) ) = 𝑥 )
22	21	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( ∗ ‘ ( ∗ ‘ 𝑥 ) ) = 𝑥 )
23	2 4 6 8 10 12 14 20 22	issrngd	⊢ ( ⊤ → ℂfld ∈ *-Ring )
24	23	mptru	⊢ ℂfld ∈ *-Ring