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

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 )