dmaddsr

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

		Ref	Expression
	Assertion	dmaddsr	$⊢ dom +_{𝑹} = 𝑹 \times 𝑹$

Step	Hyp	Ref	Expression
1		df-plr	$⊢ +_{𝑹} = \{⟨⟨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 +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹}))\}$
2	1	dmeqi	$⊢ dom +_{𝑹} = 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 +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹}))\}$
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 +_{𝑷} u, v +_{𝑷} f⟩] ~_{𝑹}))\} \subseteq 𝑹 \times 𝑹$
4	2 3	eqsstri	$⊢ dom +_{𝑹} \subseteq 𝑹 \times 𝑹$
5		0nsr	$⊢ \neg \emptyset \in 𝑹$
6		addclsr	$⊢ (x \in 𝑹 \land y \in 𝑹) \to x +_{𝑹} y \in 𝑹$
7	5 6	oprssdm	$⊢ 𝑹 \times 𝑹 \subseteq dom +_{𝑹}$
8	4 7	eqssi	$⊢ dom +_{𝑹} = 𝑹 \times 𝑹$

Metamath Proof Explorer