axaddf

Description: Addition is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axaddcl . This construction-dependent theorem should not be referenced directly; instead, use ax-addf . (Contributed by NM, 8-Feb-2005) (New usage is discouraged.)

		Ref	Expression
	Assertion	axaddf	$⊢ + : ℂ \times ℂ ⟶ ℂ$

Proof

Step	Hyp	Ref	Expression
1		moeq	$⊢ \exists^{*} z z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩$
2	1	mosubop	$⊢ \exists^{*} z \exists u \exists f (y = ⟨u, f⟩ \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩)$
3	2	mosubop	$⊢ \exists^{*} z \exists w \exists v (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩))$
4		anass	$⊢ ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩) \leftrightarrow (x = ⟨w, v⟩ \land (y = ⟨u, f⟩ \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩))$
5	4	2exbii	$⊢ \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩) \leftrightarrow \exists u \exists f (x = ⟨w, v⟩ \land (y = ⟨u, f⟩ \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩))$
6		19.42vv	$⊢ \exists u \exists f (x = ⟨w, v⟩ \land (y = ⟨u, f⟩ \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩)) \leftrightarrow (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩))$
7	5 6	bitri	$⊢ \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩) \leftrightarrow (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩))$
8	7	2exbii	$⊢ \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩) \leftrightarrow \exists w \exists v (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩))$
9	8	mobii	$⊢ \exists^{} z \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩) \leftrightarrow \exists^{} z \exists w \exists v (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩))$
10	3 9	mpbir	$⊢ \exists^{*} z \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨w +_{𝑹} u, v +_{𝑹} f⟩)$
11	10	moani	$⊢ \exists^{*} 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	11	funoprab	$⊢ Fun \{⟨⟨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⟩))\}$
13		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⟩))\}$
14	13	funeqi	$⊢ Fun + \leftrightarrow Fun \{⟨⟨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⟩))\}$
15	12 14	mpbir	$⊢ Fun +$
16	13	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⟩))\}$
17		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 ℂ$
18	16 17	eqsstri	$⊢ dom + \subseteq ℂ \times ℂ$
19		0ncn	$⊢ \neg \emptyset \in ℂ$
20		df-c	$⊢ ℂ = 𝑹 \times 𝑹$
21		oveq1	$⊢ ⟨z, w⟩ = x \to ⟨z, w⟩ + ⟨v, u⟩ = x + ⟨v, u⟩$
22	21	eleq1d	$⊢ ⟨z, w⟩ = x \to (⟨z, w⟩ + ⟨v, u⟩ \in (𝑹 \times 𝑹) \leftrightarrow x + ⟨v, u⟩ \in (𝑹 \times 𝑹))$
23		oveq2	$⊢ ⟨v, u⟩ = y \to x + ⟨v, u⟩ = x + y$
24	23	eleq1d	$⊢ ⟨v, u⟩ = y \to (x + ⟨v, u⟩ \in (𝑹 \times 𝑹) \leftrightarrow x + y \in (𝑹 \times 𝑹))$
25		addcnsr	$⊢ ((z \in 𝑹 \land w \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to ⟨z, w⟩ + ⟨v, u⟩ = ⟨z +_{𝑹} v, w +_{𝑹} u⟩$
26		addclsr	$⊢ (z \in 𝑹 \land v \in 𝑹) \to z +_{𝑹} v \in 𝑹$
27		addclsr	$⊢ (w \in 𝑹 \land u \in 𝑹) \to w +_{𝑹} u \in 𝑹$
28	26 27	anim12i	$⊢ ((z \in 𝑹 \land v \in 𝑹) \land (w \in 𝑹 \land u \in 𝑹)) \to (z +_{𝑹} v \in 𝑹 \land w +_{𝑹} u \in 𝑹)$
29	28	an4s	$⊢ ((z \in 𝑹 \land w \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to (z +_{𝑹} v \in 𝑹 \land w +_{𝑹} u \in 𝑹)$
30		opelxpi	$⊢ (z +_{𝑹} v \in 𝑹 \land w +_{𝑹} u \in 𝑹) \to ⟨z +_{𝑹} v, w +_{𝑹} u⟩ \in (𝑹 \times 𝑹)$
31	29 30	syl	$⊢ ((z \in 𝑹 \land w \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to ⟨z +_{𝑹} v, w +_{𝑹} u⟩ \in (𝑹 \times 𝑹)$
32	25 31	eqeltrd	$⊢ ((z \in 𝑹 \land w \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to ⟨z, w⟩ + ⟨v, u⟩ \in (𝑹 \times 𝑹)$
33	20 22 24 32	2optocl	$⊢ (x \in ℂ \land y \in ℂ) \to x + y \in (𝑹 \times 𝑹)$
34	33 20	eleqtrrdi	$⊢ (x \in ℂ \land y \in ℂ) \to x + y \in ℂ$
35	19 34	oprssdm	$⊢ ℂ \times ℂ \subseteq dom +$
36	18 35	eqssi	$⊢ dom + = ℂ \times ℂ$
37		df-fn	$⊢ + Fn (ℂ \times ℂ) \leftrightarrow (Fun + \land dom + = ℂ \times ℂ)$
38	15 36 37	mpbir2an	$⊢ + Fn (ℂ \times ℂ)$
39	34	rgen2	$⊢ \forall x \in ℂ \forall y \in ℂ x + y \in ℂ$
40		ffnov	$⊢ + : ℂ \times ℂ ⟶ ℂ \leftrightarrow (+ Fn (ℂ \times ℂ) \land \forall x \in ℂ \forall y \in ℂ x + y \in ℂ)$
41	38 39 40	mpbir2an	$⊢ + : ℂ \times ℂ ⟶ ℂ$

Metamath Proof Explorer

Theorem axaddf

Proof