Metamath Proof Explorer

Theorem addclsr

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

		Ref	Expression
	Assertion	addclsr	$⊢ (A \in 𝑹 \land B \in 𝑹) \to A +_{𝑹} B \in 𝑹$

Proof

Step	Hyp	Ref	Expression
1		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
2		oveq1	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to [⟨x, y⟩] ~_{𝑹} +_{𝑹} [⟨z, w⟩] ~_{𝑹} = A +_{𝑹} [⟨z, w⟩] ~_{𝑹}$
3	2	eleq1d	$⊢ [⟨x, y⟩] ~_{𝑹} = A \to ([⟨x, y⟩] ~_{𝑹} +_{𝑹} [⟨z, w⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹}) \leftrightarrow A +_{𝑹} [⟨z, w⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹}))$
4		oveq2	$⊢ [⟨z, w⟩] ~_{𝑹} = B \to A +_{𝑹} [⟨z, w⟩] ~_{𝑹} = A +_{𝑹} B$
5	4	eleq1d	$⊢ [⟨z, w⟩] ~_{𝑹} = B \to (A +_{𝑹} [⟨z, w⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹}) \leftrightarrow A +_{𝑹} B \in ((𝑷 \times 𝑷) / ~_{𝑹}))$
6		addsrpr	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to [⟨x, y⟩] ~_{𝑹} +_{𝑹} [⟨z, w⟩] ~_{𝑹} = [⟨x +_{𝑷} z, y +_{𝑷} w⟩] ~_{𝑹}$
7		addclpr	$⊢ (x \in 𝑷 \land z \in 𝑷) \to x +_{𝑷} z \in 𝑷$
8		addclpr	$⊢ (y \in 𝑷 \land w \in 𝑷) \to y +_{𝑷} w \in 𝑷$
9	7 8	anim12i	$⊢ ((x \in 𝑷 \land z \in 𝑷) \land (y \in 𝑷 \land w \in 𝑷)) \to (x +_{𝑷} z \in 𝑷 \land y +_{𝑷} w \in 𝑷)$
10	9	an4s	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to (x +_{𝑷} z \in 𝑷 \land y +_{𝑷} w \in 𝑷)$
11		opelxpi	$⊢ (x +_{𝑷} z \in 𝑷 \land y +_{𝑷} w \in 𝑷) \to ⟨x +_{𝑷} z, y +_{𝑷} w⟩ \in (𝑷 \times 𝑷)$
12		enrex	$⊢ ~_{𝑹} \in V$
13	12	ecelqsi	$⊢ ⟨x +_{𝑷} z, y +_{𝑷} w⟩ \in (𝑷 \times 𝑷) \to [⟨x +_{𝑷} z, y +_{𝑷} w⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
14	10 11 13	3syl	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to [⟨x +_{𝑷} z, y +_{𝑷} w⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
15	6 14	eqeltrd	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to [⟨x, y⟩] ~_{𝑹} +_{𝑹} [⟨z, w⟩] ~_{𝑹} \in ((𝑷 \times 𝑷) / ~_{𝑹})$
16	1 3 5 15	2ecoptocl	$⊢ (A \in 𝑹 \land B \in 𝑹) \to A +_{𝑹} B \in ((𝑷 \times 𝑷) / ~_{𝑹})$
17	16 1	eleqtrrdi	$⊢ (A \in 𝑹 \land B \in 𝑹) \to A +_{𝑹} B \in 𝑹$