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

Metamath Proof Explorer

Theorem 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 ∈ 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 mpocnfldmul ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) = ( .r ‘ ℂfld )
6 5 a1i ⊢ ( ⊤ → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) = ( .r ‘ ℂfld ) )
7 addcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 + 𝑦 ) ∈ ℂ )
8 addass ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
9 0cn ⊢ 0 ∈ ℂ
10 addlid ⊢ ( 𝑥 ∈ ℂ → ( 0 + 𝑥 ) = 𝑥 )
11 negcl ⊢ ( 𝑥 ∈ ℂ → - 𝑥 ∈ ℂ )
12 id ⊢ ( 𝑥 ∈ ℂ → 𝑥 ∈ ℂ )
13 11 12 addcomd ⊢ ( 𝑥 ∈ ℂ → ( - 𝑥 + 𝑥 ) = ( 𝑥 + - 𝑥 ) )
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 mpomulf ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) : ( ℂ × ℂ ) ⟶ ℂ
19 18 fovcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ ℂ )
20 19 3adant1 ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ∈ ℂ )
21 mulass ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) · 𝑧 ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
22 mulcl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) ∈ ℂ )
23 ovmpot ⊢ ( ( ( 𝑥 · 𝑦 ) ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 · 𝑦 ) · 𝑧 ) )
24 22 23 stoic3 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 · 𝑦 ) · 𝑧 ) )
25 simp1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → 𝑥 ∈ ℂ )
26 mulcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 · 𝑧 ) ∈ ℂ )
27 26 3adant1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 · 𝑧 ) ∈ ℂ )
28 ovmpot ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 · 𝑧 ) ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 · 𝑧 ) ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
29 25 27 28 syl2anc ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 · 𝑧 ) ) = ( 𝑥 · ( 𝑦 · 𝑧 ) ) )
30 21 24 29 3eqtr4d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 · 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 · 𝑧 ) ) )
31 ovmpot ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
32 31 3adant3 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
33 32 oveq1d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 · 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) )
34 ovmpot ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑦 · 𝑧 ) )
35 34 3adant1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑦 · 𝑧 ) )
36 35 oveq2d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) = ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 · 𝑧 ) ) )
37 30 33 36 3eqtr4d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) )
38 37 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) )
39 adddi ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 · ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
40 addcl ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 + 𝑧 ) ∈ ℂ )
41 40 3adant1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑦 + 𝑧 ) ∈ ℂ )
42 ovmpot ⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 + 𝑧 ) ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 + 𝑧 ) ) = ( 𝑥 · ( 𝑦 + 𝑧 ) ) )
43 25 41 42 syl2anc ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 + 𝑧 ) ) = ( 𝑥 · ( 𝑦 + 𝑧 ) ) )
44 ovmpot ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑥 · 𝑧 ) )
45 44 3adant2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( 𝑥 · 𝑧 ) )
46 32 45 oveq12d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) + ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) = ( ( 𝑥 · 𝑦 ) + ( 𝑥 · 𝑧 ) ) )
47 39 43 46 3eqtr4d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) + ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) )
48 47 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ( 𝑦 + 𝑧 ) ) = ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) + ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) )
49 adddir ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) · 𝑧 ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
50 ovmpot ⊢ ( ( ( 𝑥 + 𝑦 ) ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 + 𝑦 ) · 𝑧 ) )
51 7 50 stoic3 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 + 𝑦 ) · 𝑧 ) )
52 45 35 oveq12d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) + ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) = ( ( 𝑥 · 𝑧 ) + ( 𝑦 · 𝑧 ) ) )
53 49 51 52 3eqtr4d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( 𝑥 + 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) + ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) )
54 53 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑧 ∈ ℂ ) ) → ( ( 𝑥 + 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) = ( ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) + ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑧 ) ) )
55 1cnd ⊢ ( ⊤ → 1 ∈ ℂ )
56 ax-1cn ⊢ 1 ∈ ℂ
57 ovmpot ⊢ ( ( 1 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = ( 1 · 𝑥 ) )
58 56 57 mpan ⊢ ( 𝑥 ∈ ℂ → ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = ( 1 · 𝑥 ) )
59 mullid ⊢ ( 𝑥 ∈ ℂ → ( 1 · 𝑥 ) = 𝑥 )
60 58 59 eqtrd ⊢ ( 𝑥 ∈ ℂ → ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = 𝑥 )
61 60 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 1 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = 𝑥 )
62 ovmpot ⊢ ( ( 𝑥 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = ( 𝑥 · 1 ) )
63 56 62 mpan2 ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = ( 𝑥 · 1 ) )
64 mulrid ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · 1 ) = 𝑥 )
65 63 64 eqtrd ⊢ ( 𝑥 ∈ ℂ → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = 𝑥 )
66 65 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 1 ) = 𝑥 )
67 mulcom ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 · 𝑦 ) = ( 𝑦 · 𝑥 ) )
68 ovmpot ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = ( 𝑦 · 𝑥 ) )
69 68 ancoms ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = ( 𝑦 · 𝑥 ) )
70 67 31 69 3eqtr4d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) )
71 70 3adant1 ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑦 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) )
72 2 4 6 17 20 38 48 54 55 61 66 71 iscrngd ⊢ ( ⊤ → ℂfld ∈ CRing )
73 72 mptru ⊢ ℂfld ∈ CRing