Metamath Proof Explorer

Theorem addcnsr

Description: Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	addcnsr	$⊢ ((A \in 𝑹 \land B \in 𝑹) \land (C \in 𝑹 \land D \in 𝑹)) \to ⟨A, B⟩ + ⟨C, D⟩ = ⟨A +_{𝑹} C, B +_{𝑹} D⟩$

Proof

Step	Hyp	Ref	Expression
1		opex	$⊢ ⟨A +_{𝑹} C, B +_{𝑹} D⟩ \in V$
2		oveq1	$⊢ w = A \to w +_{𝑹} u = A +_{𝑹} u$
3		oveq1	$⊢ v = B \to v +_{𝑹} f = B +_{𝑹} f$
4		opeq12	$⊢ (w +_{𝑹} u = A +_{𝑹} u \land v +_{𝑹} f = B +_{𝑹} f) \to ⟨w +_{𝑹} u, v +_{𝑹} f⟩ = ⟨A +_{𝑹} u, B +_{𝑹} f⟩$
5	2 3 4	syl2an	$⊢ (w = A \land v = B) \to ⟨w +_{𝑹} u, v +_{𝑹} f⟩ = ⟨A +_{𝑹} u, B +_{𝑹} f⟩$
6		oveq2	$⊢ u = C \to A +_{𝑹} u = A +_{𝑹} C$
7		oveq2	$⊢ f = D \to B +_{𝑹} f = B +_{𝑹} D$
8		opeq12	$⊢ (A +_{𝑹} u = A +_{𝑹} C \land B +_{𝑹} f = B +_{𝑹} D) \to ⟨A +_{𝑹} u, B +_{𝑹} f⟩ = ⟨A +_{𝑹} C, B +_{𝑹} D⟩$
9	6 7 8	syl2an	$⊢ (u = C \land f = D) \to ⟨A +_{𝑹} u, B +_{𝑹} f⟩ = ⟨A +_{𝑹} C, B +_{𝑹} D⟩$
10	5 9	sylan9eq	$⊢ ((w = A \land v = B) \land (u = C \land f = D)) \to ⟨w +_{𝑹} u, v +_{𝑹} f⟩ = ⟨A +_{𝑹} C, B +_{𝑹} D⟩$
11		df-add	$⊢ + = \{⟨⟨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⟩))\}$
12		df-c	$⊢ ℂ = 𝑹 \times 𝑹$
13	12	eleq2i	$⊢ x \in ℂ \leftrightarrow x \in (𝑹 \times 𝑹)$
14	12	eleq2i	$⊢ y \in ℂ \leftrightarrow y \in (𝑹 \times 𝑹)$
15	13 14	anbi12i	$⊢ (x \in ℂ \land y \in ℂ) \leftrightarrow (x \in (𝑹 \times 𝑹) \land y \in (𝑹 \times 𝑹))$
16	15	anbi1i	$⊢ ((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⟩)) \leftrightarrow ((x \in (𝑹 \times 𝑹) \land y \in (𝑹 \times 𝑹)) \land \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩))$
17	16	oprabbii	$⊢ \{⟨⟨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⟩))\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in (𝑹 \times 𝑹) \land y \in (𝑹 \times 𝑹)) \land \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩))\}$
18	11 17	eqtri	$⊢ + = \{⟨⟨x, y⟩, z⟩ \| ((x \in (𝑹 \times 𝑹) \land y \in (𝑹 \times 𝑹)) \land \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩))\}$
19	1 10 18	ov3	$⊢ ((A \in 𝑹 \land B \in 𝑹) \land (C \in 𝑹 \land D \in 𝑹)) \to ⟨A, B⟩ + ⟨C, D⟩ = ⟨A +_{𝑹} C, B +_{𝑹} D⟩$