dmmulsr

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

		Ref	Expression
	Assertion	dmmulsr	$⊢ dom \cdot_{𝑹} = 𝑹 \times 𝑹$

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

Metamath Proof Explorer