Theorem cnflddiv

Description: The division operation in the field of complex numbers. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 2-Dec-2014) Avoid ax-mulf . (Revised by GG, 30-Apr-2025)

	Ref	Expression
Assertion	cnflddiv	⊢ / = ( /r ‘ ℂfld )

Proof

Step	Hyp	Ref	Expression
1		cnring	⊢ ℂfld ∈ Ring
2		cnfldbas	⊢ ℂ = ( Base ‘ ℂfld )
3		cnfld0	⊢ 0 = ( 0g ‘ ℂfld )
4		cndrng	⊢ ℂfld ∈ DivRing
5	2 3 4	drngui	⊢ ( ℂ ∖ { 0 } ) = ( Unit ‘ ℂfld )
6		eqid	⊢ ( /r ‘ ℂfld ) = ( /r ‘ ℂfld )
7	2 5 6	dvrcl	⊢ ( ( ℂfld ∈ Ring ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) ∈ ℂ )
8	1 7	mp3an1	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) ∈ ℂ )
9		difssd	⊢ ( 𝑥 ∈ ℂ → ( ℂ ∖ { 0 } ) ⊆ ℂ )
10	9	sselda	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ∈ ℂ )
11		ovmpot	⊢ ( ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) · 𝑦 ) )
12	8 10 11	syl2anc	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) · 𝑦 ) )
13		mpocnfldmul	⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) = ( .r ‘ ℂfld )
14	2 5 6 13	dvrcan1	⊢ ( ( ℂfld ∈ Ring ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = 𝑥 )
15	1 14	mp3an1	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) 𝑦 ) = 𝑥 )
16	12 15	eqtr3d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) · 𝑦 ) = 𝑥 )
17	16	oveq1d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) · 𝑦 ) / 𝑦 ) = ( 𝑥 / 𝑦 ) )
18		eldifsni	⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) → 𝑦 ≠ 0 )
19	18	adantl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ≠ 0 )
20	8 10 19	divcan4d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) · 𝑦 ) / 𝑦 ) = ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) )
21	17 20	eqtr3d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 / 𝑦 ) = ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) )
22		simpl	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ∈ ℂ )
23		divval	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 𝑥 / 𝑦 ) = ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
24	22 10 19 23	syl3anc	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 / 𝑦 ) = ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
25	21 24	eqtr3d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) = ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
26		eqid	⊢ ( .r ‘ ℂfld ) = ( .r ‘ ℂfld )
27		eqid	⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld )
28	2 26 5 27 6	dvrval	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) = ( 𝑥 ( .r ‘ ℂfld ) ( ( invr ‘ ℂfld ) ‘ 𝑦 ) ) )
29	25 28	eqtr3d	⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) = ( 𝑥 ( .r ‘ ℂfld ) ( ( invr ‘ ℂfld ) ‘ 𝑦 ) ) )
30	29	mpoeq3ia	⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 ( .r ‘ ℂfld ) ( ( invr ‘ ℂfld ) ‘ 𝑦 ) ) )
31		df-div	⊢ / = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
32	2 26 5 27 6	dvrfval	⊢ ( /r ‘ ℂfld ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 ( .r ‘ ℂfld ) ( ( invr ‘ ℂfld ) ‘ 𝑦 ) ) )
33	30 31 32	3eqtr4i	⊢ / = ( /r ‘ ℂfld )