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	$⊢ \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	2 5 6	dvrcl	$⊢ (ℂ_{fld} \in Ring \land x \in ℂ \land y \in (ℂ ∖ \{0\})) \to x /_{r} (ℂ_{fld}) y \in ℂ$
8	1 7	mp3an1	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to x /_{r} (ℂ_{fld}) y \in ℂ$
9		difssd	$⊢ x \in ℂ \to ℂ ∖ \{0\} \subseteq ℂ$
10	9	sselda	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \in ℂ$
11		ovmpot	$⊢ (x /_{r} (ℂ_{fld}) y \in ℂ \land y \in ℂ) \to (x /_{r} (ℂ_{fld}) y) (u \in ℂ, v \in ℂ ⟼ u v) y = (x /_{r} (ℂ_{fld}) y) y$
12	8 10 11	syl2anc	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to (x /_{r} (ℂ_{fld}) y) (u \in ℂ, v \in ℂ ⟼ u v) y = (x /_{r} (ℂ_{fld}) y) y$
13		mpocnfldmul	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) = \cdot_{ℂ_{fld}}$
14	2 5 6 13	dvrcan1	$⊢ (ℂ_{fld} \in Ring \land x \in ℂ \land y \in (ℂ ∖ \{0\})) \to (x /_{r} (ℂ_{fld}) y) (u \in ℂ, v \in ℂ ⟼ u v) y = x$
15	1 14	mp3an1	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to (x /_{r} (ℂ_{fld}) y) (u \in ℂ, v \in ℂ ⟼ u v) y = x$
16	12 15	eqtr3d	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to (x /_{r} (ℂ_{fld}) y) y = x$
17	16	oveq1d	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{(x /_{r} (ℂ_{fld}) y) y}{y} = \frac{x}{y}$
18		eldifsni	$⊢ y \in (ℂ ∖ \{0\}) \to y \neq 0$
19	18	adantl	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to y \neq 0$
20	8 10 19	divcan4d	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{(x /_{r} (ℂ_{fld}) y) y}{y} = x /_{r} (ℂ_{fld}) y$
21	17 20	eqtr3d	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{x}{y} = x /_{r} (ℂ_{fld}) y$
22		simpl	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to x \in ℂ$
23		divval	$⊢ (x \in ℂ \land y \in ℂ \land y \neq 0) \to \frac{x}{y} = (ι z \in ℂ \| y z = x)$
24	22 10 19 23	syl3anc	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to \frac{x}{y} = (ι z \in ℂ \| y z = x)$
25	21 24	eqtr3d	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to x /_{r} (ℂ_{fld}) y = (ι z \in ℂ \| y z = x)$
26		eqid	$⊢ \cdot_{ℂ_{fld}} = \cdot_{ℂ_{fld}}$
27		eqid	$⊢ {inv}_{r} (ℂ_{fld}) = {inv}_{r} (ℂ_{fld})$
28	2 26 5 27 6	dvrval	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to x /_{r} (ℂ_{fld}) y = x \cdot_{ℂ_{fld}} {inv}_{r} (ℂ_{fld}) (y)$
29	25 28	eqtr3d	$⊢ (x \in ℂ \land y \in (ℂ ∖ \{0\})) \to (ι z \in ℂ \| y z = x) = x \cdot_{ℂ_{fld}} {inv}_{r} (ℂ_{fld}) (y)$
30	29	mpoeq3ia	$⊢ (x \in ℂ, y \in (ℂ ∖ \{0\}) ⟼ (ι z \in ℂ \| y z = x)) = (x \in ℂ, y \in (ℂ ∖ \{0\}) ⟼ x \cdot_{ℂ_{fld}} {inv}_{r} (ℂ_{fld}) (y))$
31		df-div	$⊢ \div = (x \in ℂ, y \in (ℂ ∖ \{0\}) ⟼ (ι z \in ℂ \| y z = x))$
32	2 26 5 27 6	dvrfval	$⊢ /_{r} (ℂ_{fld}) = (x \in ℂ, y \in (ℂ ∖ \{0\}) ⟼ x \cdot_{ℂ_{fld}} {inv}_{r} (ℂ_{fld}) (y))$
33	30 31 32	3eqtr4i	$⊢ \div = /_{r} (ℂ_{fld})$

Metamath Proof Explorer

Theorem cnflddiv

Proof