axmulf

Description: Multiplication is an operation on the complex numbers. This is the construction-dependent version of ax-mulf and it should not be referenced outside the construction. We generally prefer to develop our theory using the less specific mulcl . (Contributed by NM, 8-Feb-2005) (New usage is discouraged.)

		Ref	Expression
	Assertion	axmulf	$⊢ \times : ℂ \times ℂ ⟶ ℂ$

Proof

Step	Hyp	Ref	Expression
1		moeq	$⊢ \exists^{*} z z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩$
2	1	mosubop	$⊢ \exists^{*} z \exists u \exists f (y = ⟨u, f⟩ \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩)$
3	2	mosubop	$⊢ \exists^{*} z \exists w \exists v (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩))$
4		anass	$⊢ ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩) \leftrightarrow (x = ⟨w, v⟩ \land (y = ⟨u, f⟩ \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩))$
5	4	2exbii	$⊢ \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩) \leftrightarrow \exists u \exists f (x = ⟨w, v⟩ \land (y = ⟨u, f⟩ \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩))$
6		19.42vv	$⊢ \exists u \exists f (x = ⟨w, v⟩ \land (y = ⟨u, f⟩ \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩)) \leftrightarrow (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩))$
7	5 6	bitri	$⊢ \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩) \leftrightarrow (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩))$
8	7	2exbii	$⊢ \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩) \leftrightarrow \exists w \exists v (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩))$
9	8	mobii	$⊢ \exists^{} z \exists w \exists v \exists u \exists f ((x = ⟨w, v⟩ \land y = ⟨u, f⟩) \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩) \leftrightarrow \exists^{} z \exists w \exists v (x = ⟨w, v⟩ \land \exists u \exists f (y = ⟨u, f⟩ \land z = ⟨(w \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} 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 \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} 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 \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} 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 \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩))\}$
13		df-mul	$⊢ \times = \{⟨⟨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) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩))\}$
14	13	funeqi	$⊢ Fun \times \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 \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩))\}$
15	12 14	mpbir	$⊢ Fun \times$
16	13	dmeqi	$⊢ dom \times = 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) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} 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 \cdot_{𝑹} u) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (v \cdot_{𝑹} f)), (v \cdot_{𝑹} u) +_{𝑹} (w \cdot_{𝑹} f)⟩))\} \subseteq ℂ \times ℂ$
18	16 17	eqsstri	$⊢ dom \times \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		mulcnsr	$⊢ ((z \in 𝑹 \land w \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to ⟨z, w⟩ ⟨v, u⟩ = ⟨(z \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (w \cdot_{𝑹} u)), (w \cdot_{𝑹} v) +_{𝑹} (z \cdot_{𝑹} u)⟩$
26		mulclsr	$⊢ (z \in 𝑹 \land v \in 𝑹) \to z \cdot_{𝑹} v \in 𝑹$
27		m1r	$⊢ {-1}_{𝑹} \in 𝑹$
28		mulclsr	$⊢ (w \in 𝑹 \land u \in 𝑹) \to w \cdot_{𝑹} u \in 𝑹$
29		mulclsr	$⊢ ({-1}_{𝑹} \in 𝑹 \land w \cdot_{𝑹} u \in 𝑹) \to {-1}_{𝑹} \cdot_{𝑹} (w \cdot_{𝑹} u) \in 𝑹$
30	27 28 29	sylancr	$⊢ (w \in 𝑹 \land u \in 𝑹) \to {-1}_{𝑹} \cdot_{𝑹} (w \cdot_{𝑹} u) \in 𝑹$
31		addclsr	$⊢ (z \cdot_{𝑹} v \in 𝑹 \land {-1}_{𝑹} \cdot_{𝑹} (w \cdot_{𝑹} u) \in 𝑹) \to (z \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (w \cdot_{𝑹} u)) \in 𝑹$
32	26 30 31	syl2an	$⊢ ((z \in 𝑹 \land v \in 𝑹) \land (w \in 𝑹 \land u \in 𝑹)) \to (z \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (w \cdot_{𝑹} u)) \in 𝑹$
33	32	an4s	$⊢ ((z \in 𝑹 \land w \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to (z \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (w \cdot_{𝑹} u)) \in 𝑹$
34		mulclsr	$⊢ (w \in 𝑹 \land v \in 𝑹) \to w \cdot_{𝑹} v \in 𝑹$
35		mulclsr	$⊢ (z \in 𝑹 \land u \in 𝑹) \to z \cdot_{𝑹} u \in 𝑹$
36		addclsr	$⊢ (w \cdot_{𝑹} v \in 𝑹 \land z \cdot_{𝑹} u \in 𝑹) \to (w \cdot_{𝑹} v) +_{𝑹} (z \cdot_{𝑹} u) \in 𝑹$
37	34 35 36	syl2anr	$⊢ ((z \in 𝑹 \land u \in 𝑹) \land (w \in 𝑹 \land v \in 𝑹)) \to (w \cdot_{𝑹} v) +_{𝑹} (z \cdot_{𝑹} u) \in 𝑹$
38	37	an42s	$⊢ ((z \in 𝑹 \land w \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to (w \cdot_{𝑹} v) +_{𝑹} (z \cdot_{𝑹} u) \in 𝑹$
39	33 38	opelxpd	$⊢ ((z \in 𝑹 \land w \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to ⟨(z \cdot_{𝑹} v) +_{𝑹} ({-1}_{𝑹} \cdot_{𝑹} (w \cdot_{𝑹} u)), (w \cdot_{𝑹} v) +_{𝑹} (z \cdot_{𝑹} u)⟩ \in (𝑹 \times 𝑹)$
40	25 39	eqeltrd	$⊢ ((z \in 𝑹 \land w \in 𝑹) \land (v \in 𝑹 \land u \in 𝑹)) \to ⟨z, w⟩ ⟨v, u⟩ \in (𝑹 \times 𝑹)$
41	20 22 24 40	2optocl	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in (𝑹 \times 𝑹)$
42	41 20	eleqtrrdi	$⊢ (x \in ℂ \land y \in ℂ) \to x y \in ℂ$
43	19 42	oprssdm	$⊢ ℂ \times ℂ \subseteq dom \times$
44	18 43	eqssi	$⊢ dom \times = ℂ \times ℂ$
45		df-fn	$⊢ \times Fn (ℂ \times ℂ) \leftrightarrow (Fun \times \land dom \times = ℂ \times ℂ)$
46	15 44 45	mpbir2an	$⊢ \times Fn (ℂ \times ℂ)$
47	42	rgen2	$⊢ \forall x \in ℂ \forall y \in ℂ x y \in ℂ$
48		ffnov	$⊢ \times : ℂ \times ℂ ⟶ ℂ \leftrightarrow (\times Fn (ℂ \times ℂ) \land \forall x \in ℂ \forall y \in ℂ x y \in ℂ)$
49	46 47 48	mpbir2an	$⊢ \times : ℂ \times ℂ ⟶ ℂ$

Metamath Proof Explorer

Theorem axmulf

Proof