Theorem dmmulsr

Description: Domain of multiplication on signed reals. (Contributed by NM, 25-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	dmmulsr	$$⊢\mathrm{dom}{\cdot }_{𝑹}=𝑹\times 𝑹$$

Proof

Step	Hyp	Ref	Expression
1		df-mr	$$⊢{\cdot }_{𝑹}=\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in 𝑹\wedge y\in 𝑹\right)\wedge \exists w\exists v\exists u\exists f\left(\left(x=\left[⟨w,v⟩\right]{~}_{𝑹}\wedge y=\left[⟨u,f⟩\right]{~}_{𝑹}\right)\wedge z=\left[⟨\left(w{\cdot }_{𝑷}u\right){+}_{𝑷}\left(v{\cdot }_{𝑷}f\right),\left(w{\cdot }_{𝑷}f\right){+}_{𝑷}\left(v{\cdot }_{𝑷}u\right)⟩\right]{~}_{𝑹}\right)\right)\right\}$$
2	1	dmeqi	$$⊢\mathrm{dom}{\cdot }_{𝑹}=\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in 𝑹\wedge y\in 𝑹\right)\wedge \exists w\exists v\exists u\exists f\left(\left(x=\left[⟨w,v⟩\right]{~}_{𝑹}\wedge y=\left[⟨u,f⟩\right]{~}_{𝑹}\right)\wedge z=\left[⟨\left(w{\cdot }_{𝑷}u\right){+}_{𝑷}\left(v{\cdot }_{𝑷}f\right),\left(w{\cdot }_{𝑷}f\right){+}_{𝑷}\left(v{\cdot }_{𝑷}u\right)⟩\right]{~}_{𝑹}\right)\right)\right\}$$
3		dmoprabss	$$⊢\mathrm{dom}\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in 𝑹\wedge y\in 𝑹\right)\wedge \exists w\exists v\exists u\exists f\left(\left(x=\left[⟨w,v⟩\right]{~}_{𝑹}\wedge y=\left[⟨u,f⟩\right]{~}_{𝑹}\right)\wedge z=\left[⟨\left(w{\cdot }_{𝑷}u\right){+}_{𝑷}\left(v{\cdot }_{𝑷}f\right),\left(w{\cdot }_{𝑷}f\right){+}_{𝑷}\left(v{\cdot }_{𝑷}u\right)⟩\right]{~}_{𝑹}\right)\right)\right\}\subseteq 𝑹\times 𝑹$$
4	2 3	eqsstri	$$⊢\mathrm{dom}{\cdot }_{𝑹}\subseteq 𝑹\times 𝑹$$
5		0nsr	$$⊢\neg \varnothing \in 𝑹$$
6		mulclsr	$$⊢\left(x\in 𝑹\wedge y\in 𝑹\right)\to x{\cdot }_{𝑹}y\in 𝑹$$
7	5 6	oprssdm	$$⊢𝑹\times 𝑹\subseteq \mathrm{dom}{\cdot }_{𝑹}$$
8	4 7	eqssi	$$⊢\mathrm{dom}{\cdot }_{𝑹}=𝑹\times 𝑹$$