This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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