Theorem xdivval

Description: Value of division: the (unique) element x such that ( B x. x ) = A . This is meaningful only when B is nonzero. (Contributed by Thierry Arnoux, 17-Dec-2016)

	Ref	Expression
Assertion	xdivval	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\wedge B\ne 0\right)\to A{÷}_{𝑒}B=\left(\iota x\in {ℝ}^{*}|B{\cdot }_{𝑒}x=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		eldifsn	$$⊢B\in \left(ℝ\setminus \left\{0\right\}\right)\leftrightarrow \left(B\in ℝ\wedge B\ne 0\right)$$
2		simpl	$$⊢\left(y=A\wedge x\in {ℝ}^{*}\right)\to y=A$$
3	2	eqeq2d	$$⊢\left(y=A\wedge x\in {ℝ}^{*}\right)\to \left(z{\cdot }_{𝑒}x=y\leftrightarrow z{\cdot }_{𝑒}x=A\right)$$
4	3	riotabidva	$$⊢y=A\to \left(\iota x\in {ℝ}^{*}|z{\cdot }_{𝑒}x=y\right)=\left(\iota x\in {ℝ}^{*}|z{\cdot }_{𝑒}x=A\right)$$
5		simpl	$$⊢\left(z=B\wedge x\in {ℝ}^{*}\right)\to z=B$$
6	5	oveq1d	$$⊢\left(z=B\wedge x\in {ℝ}^{*}\right)\to z{\cdot }_{𝑒}x=B{\cdot }_{𝑒}x$$
7	6	eqeq1d	$$⊢\left(z=B\wedge x\in {ℝ}^{*}\right)\to \left(z{\cdot }_{𝑒}x=A\leftrightarrow B{\cdot }_{𝑒}x=A\right)$$
8	7	riotabidva	$$⊢z=B\to \left(\iota x\in {ℝ}^{*}|z{\cdot }_{𝑒}x=A\right)=\left(\iota x\in {ℝ}^{*}|B{\cdot }_{𝑒}x=A\right)$$
9		df-xdiv	$$⊢{÷}_{𝑒}=\left(y\in {ℝ}^{*},z\in \left(ℝ\setminus \left\{0\right\}\right)⟼\left(\iota x\in {ℝ}^{*}|z{\cdot }_{𝑒}x=y\right)\right)$$
10		riotaex	$$⊢\left(\iota x\in {ℝ}^{*}|B{\cdot }_{𝑒}x=A\right)\in \mathrm{V}$$
11	4 8 9 10	ovmpo	$$⊢\left(A\in {ℝ}^{*}\wedge B\in \left(ℝ\setminus \left\{0\right\}\right)\right)\to A{÷}_{𝑒}B=\left(\iota x\in {ℝ}^{*}|B{\cdot }_{𝑒}x=A\right)$$
12	1 11	sylan2br	$$⊢\left(A\in {ℝ}^{*}\wedge \left(B\in ℝ\wedge B\ne 0\right)\right)\to A{÷}_{𝑒}B=\left(\iota x\in {ℝ}^{*}|B{\cdot }_{𝑒}x=A\right)$$
13	12	3impb	$$⊢\left(A\in {ℝ}^{*}\wedge B\in ℝ\wedge B\ne 0\right)\to A{÷}_{𝑒}B=\left(\iota x\in {ℝ}^{*}|B{\cdot }_{𝑒}x=A\right)$$