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)

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 cnfldmul ⊢ · = ( .r ‘ ℂfld )
8 2 5 6 7 dvrcan1 ⊢ ( ( ℂfld ∈ Ring ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) · 𝑦 ) = 𝑥 )
9 1 8 mp3an1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) · 𝑦 ) = 𝑥 )
10 9 oveq1d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) · 𝑦 ) / 𝑦 ) = ( 𝑥 / 𝑦 ) )
11 2 5 6 dvrcl ⊢ ( ( ℂfld ∈ Ring ∧ 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) ∈ ℂ )
12 1 11 mp3an1 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) ∈ ℂ )
13 simpr ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ∈ ( ℂ ∖ { 0 } ) )
14 eldifsn ⊢ ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
15 13 14 sylib ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
16 15 simpld ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ∈ ℂ )
17 15 simprd ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ≠ 0 )
18 12 16 17 divcan4d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ( ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) · 𝑦 ) / 𝑦 ) = ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) )
19 10 18 eqtr3d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 / 𝑦 ) = ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) )
20 simpl ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ∈ ℂ )
21 divval ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 𝑥 / 𝑦 ) = ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
22 20 16 17 21 syl3anc ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 / 𝑦 ) = ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
23 19 22 eqtr3d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) = ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
24 eqid ⊢ ( invr ‘ ℂfld ) = ( invr ‘ ℂfld )
25 2 7 5 24 6 dvrval ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ( /r ‘ ℂfld ) 𝑦 ) = ( 𝑥 · ( ( invr ‘ ℂfld ) ‘ 𝑦 ) ) )
26 23 25 eqtr3d ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) = ( 𝑥 · ( ( invr ‘ ℂfld ) ‘ 𝑦 ) ) )
27 26 mpoeq3ia ⊢ ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · ( ( invr ‘ ℂfld ) ‘ 𝑦 ) ) )
28 df-div ⊢ / = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℂ ( 𝑦 · 𝑧 ) = 𝑥 ) )
29 2 7 5 24 6 dvrfval ⊢ ( /r ‘ ℂfld ) = ( 𝑥 ∈ ℂ , 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 · ( ( invr ‘ ℂfld ) ‘ 𝑦 ) ) )
30 27 28 29 3eqtr4i ⊢ / = ( /r ‘ ℂfld )