Metamath Proof Explorer


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 )