Definition df-xdiv

Description: Define division over extended real numbers. (Contributed by Thierry Arnoux, 17-Dec-2016)

	Ref	Expression
Assertion	df-xdiv	⊢ /𝑒 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ( ℝ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℝ* ( 𝑦 ·e 𝑧 ) = 𝑥 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cxdiv	⊢ /𝑒
1		vx	⊢ 𝑥
2		cxr	⊢ ℝ*
3		vy	⊢ 𝑦
4		cr	⊢ ℝ
5		cc0	⊢ 0
6	5	csn	⊢ { 0 }
7	4 6	cdif	⊢ ( ℝ ∖ { 0 } )
8		vz	⊢ 𝑧
9	3	cv	⊢ 𝑦
10		cxmu	⊢ ·e
11	8	cv	⊢ 𝑧
12	9 11 10	co	⊢ ( 𝑦 ·e 𝑧 )
13	1	cv	⊢ 𝑥
14	12 13	wceq	⊢ ( 𝑦 ·e 𝑧 ) = 𝑥
15	14 8 2	crio	⊢ ( ℩ 𝑧 ∈ ℝ* ( 𝑦 ·e 𝑧 ) = 𝑥 )
16	1 3 2 7 15	cmpo	⊢ ( 𝑥 ∈ ℝ* , 𝑦 ∈ ( ℝ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℝ* ( 𝑦 ·e 𝑧 ) = 𝑥 ) )
17	0 16	wceq	⊢ /𝑒 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ( ℝ ∖ { 0 } ) ↦ ( ℩ 𝑧 ∈ ℝ* ( 𝑦 ·e 𝑧 ) = 𝑥 ) )