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	$⊢ \div = /_{r} (ℂ_{fld})$

Proof

Step	Hyp	Ref	Expression
1		cnring	$⊢ ℂ_{fld} \in Ring$
2		cnfldbas	$⊢ ℂ = {Base}_{ℂ_{fld}}$
3		cnfld0	$⊢ 0 = 0_{ℂ_{fld}}$
4		cndrng	$⊢ ℂ_{fld} \in DivRing$
5	2 3 4	drngui	$⊢ ℂ ∖ \{0\} = Unit (ℂ_{fld})$
6		eqid	$⊢ /_{r} (ℂ_{fld}) = /_{r} (ℂ_{fld})$
7		cnfldmul	$⊢ \times = \cdot_{ℂ_{fld}}$
8	2 5 6 7	dvrcan1	$⊢ (ℂ_{fld} \in Ring \land x \in ℂ \land y \in (ℂ ∖ \{0\})) \to (x /_{r} (ℂ_{fld}) y) y = x$
9	1 8	mp3an1	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to (x /_{r} (ℂ_{fld}) y) y = x$
10	9	oveq1d	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{(x /_{r} (ℂ_{fld}) y) y}{y} = \frac{x}{y}$
11	2 5 6	dvrcl	$⊢ (ℂ_{fld} \in Ring \land x \in ℂ \land y \in (ℂ ∖ \{0\})) \to x /_{r} (ℂ_{fld}) y \in ℂ$
12	1 11	mp3an1	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to x /_{r} (ℂ_{fld}) y \in ℂ$
13		simpr	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \in (ℂ ∖ \{0\})$
14		eldifsn	$⊢ y \in (ℂ ∖ \{0\}) \leftrightarrow (y \in ℂ \land y \neq 0)$
15	13 14	sylib	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to (y \in ℂ \land y \neq 0)$
16	15	simpld	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \in ℂ$
17	15	simprd	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \neq 0$
18	12 16 17	divcan4d	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{(x /_{r} (ℂ_{fld}) y) y}{y} = x /_{r} (ℂ_{fld}) y$
19	10 18	eqtr3d	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{x}{y} = x /_{r} (ℂ_{fld}) y$
20		simpl	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to x \in ℂ$
21		divval	$⊢ (x \in ℂ \land y \in ℂ \land y \neq 0) \to \frac{x}{y} = (ι z \in ℂ \| y z = x)$
22	20 16 17 21	syl3anc	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{x}{y} = (ι z \in ℂ \| y z = x)$
23	19 22	eqtr3d	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to x /_{r} (ℂ_{fld}) y = (ι z \in ℂ \| y z = x)$
24		eqid	$⊢ {inv}_{r} (ℂ_{fld}) = {inv}_{r} (ℂ_{fld})$
25	2 7 5 24 6	dvrval	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to x /_{r} (ℂ_{fld}) y = x {inv}_{r} (ℂ_{fld}) (y)$
26	23 25	eqtr3d	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to (ι z \in ℂ \| y z = x) = x {inv}_{r} (ℂ_{fld}) (y)$
27	26	mpoeq3ia	$⊢ (x \in ℂ, y \in (ℂ ∖ \{0\}) ⟼ (ι z \in ℂ \| y z = x)) = (x \in ℂ, y \in (ℂ ∖ \{0\}) ⟼ x {inv}_{r} (ℂ_{fld}) (y))$
28		df-div	$⊢ \div = (x \in ℂ, y \in (ℂ ∖ \{0\}) ⟼ (ι z \in ℂ \| y z = x))$
29	2 7 5 24 6	dvrfval	$⊢ /_{r} (ℂ_{fld}) = (x \in ℂ, y \in (ℂ ∖ \{0\}) ⟼ x {inv}_{r} (ℂ_{fld}) (y))$
30	27 28 29	3eqtr4i	$⊢ \div = /_{r} (ℂ_{fld})$

Metamath Proof Explorer

Theorem cnflddiv

Proof