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

Metamath Proof Explorer

Theorem cndrng

Description: The complex numbers form a division ring. (Contributed by Stefan O'Rear, 27-Nov-2014) Avoid ax-mulf . (Revised by GG, 30-Apr-2025)

Ref Expression
Assertion cndrng ℂfld ∈ DivRing

Proof

Step Hyp Ref Expression
1 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
2 1 a1i ⊢ ( ⊤ → ℂ = ( Base ‘ ℂfld ) )
3 mpocnfldmul ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) = ( .r ‘ ℂfld )
4 3 a1i ⊢ ( ⊤ → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) = ( .r ‘ ℂfld ) )
5 cnfld0 ⊢ 0 = ( 0g ‘ ℂfld )
6 5 a1i ⊢ ( ⊤ → 0 = ( 0g ‘ ℂfld ) )
7 cnfld1 ⊢ 1 = ( 1r ‘ ℂfld )
8 7 a1i ⊢ ( ⊤ → 1 = ( 1r ‘ ℂfld ) )
9 cnring ⊢ ℂfld ∈ Ring
10 9 a1i ⊢ ( ⊤ → ℂfld ∈ Ring )
11 ovmpot ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
12 11 ad2ant2r ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( 𝑥 · 𝑦 ) )
13 mulne0 ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 · 𝑦 ) ≠ 0 )
14 12 13 eqnetrd ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ≠ 0 )
15 14 3adant1 ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) ) → ( 𝑥 ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) ≠ 0 )
16 ax-1ne0 ⊢ 1 ≠ 0
17 16 a1i ⊢ ( ⊤ → 1 ≠ 0 )
18 reccl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 1 / 𝑥 ) ∈ ℂ )
19 18 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( 1 / 𝑥 ) ∈ ℂ )
20 simpl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → 𝑥 ∈ ℂ )
21 ovmpot ⊢ ( ( ( 1 / 𝑥 ) ∈ ℂ ∧ 𝑥 ∈ ℂ ) → ( ( 1 / 𝑥 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = ( ( 1 / 𝑥 ) · 𝑥 ) )
22 18 20 21 syl2anc ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( ( 1 / 𝑥 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = ( ( 1 / 𝑥 ) · 𝑥 ) )
23 recid2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( ( 1 / 𝑥 ) · 𝑥 ) = 1 )
24 22 23 eqtrd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( ( 1 / 𝑥 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = 1 )
25 24 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( 1 / 𝑥 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑥 ) = 1 )
26 2 4 6 8 10 15 17 19 25 isdrngd ⊢ ( ⊤ → ℂfld ∈ DivRing )
27 26 mptru ⊢ ℂfld ∈ DivRing