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