Definition df-mul

Description: Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	df-mul	$$⊢\times =\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in ℂ\wedge y\in ℂ\right)\wedge \exists w\exists v\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨\left(w{\cdot }_{𝑹}u\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right),\left(v{\cdot }_{𝑹}u\right){+}_{𝑹}\left(w{\cdot }_{𝑹}f\right)⟩\right)\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmul	$$class\times$$
1		vx	$$setvarx$$
2		vy	$$setvary$$
3		vz	$$setvarz$$
4	1	cv	$$setvarx$$
5		cc	$$classℂ$$
6	4 5	wcel	$$wffx\in ℂ$$
7	2	cv	$$setvary$$
8	7 5	wcel	$$wffy\in ℂ$$
9	6 8	wa	$$wff\left(x\in ℂ\wedge y\in ℂ\right)$$
10		vw	$$setvarw$$
11		vv	$$setvarv$$
12		vu	$$setvaru$$
13		vf	$$setvarf$$
14	10	cv	$$setvarw$$
15	11	cv	$$setvarv$$
16	14 15	cop	$$class⟨w,v⟩$$
17	4 16	wceq	$$wffx=⟨w,v⟩$$
18	12	cv	$$setvaru$$
19	13	cv	$$setvarf$$
20	18 19	cop	$$class⟨u,f⟩$$
21	7 20	wceq	$$wffy=⟨u,f⟩$$
22	17 21	wa	$$wff\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)$$
23	3	cv	$$setvarz$$
24		cmr	$$class{\cdot }_{𝑹}$$
25	14 18 24	co	$$class\left(w{\cdot }_{𝑹}u\right)$$
26		cplr	$$class{+}_{𝑹}$$
27		cm1r	$$class{-1}_{𝑹}$$
28	15 19 24	co	$$class\left(v{\cdot }_{𝑹}f\right)$$
29	27 28 24	co	$$class\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right)$$
30	25 29 26	co	$$class\left(\left(w{\cdot }_{𝑹}u\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right)\right)$$
31	15 18 24	co	$$class\left(v{\cdot }_{𝑹}u\right)$$
32	14 19 24	co	$$class\left(w{\cdot }_{𝑹}f\right)$$
33	31 32 26	co	$$class\left(\left(v{\cdot }_{𝑹}u\right){+}_{𝑹}\left(w{\cdot }_{𝑹}f\right)\right)$$
34	30 33	cop	$$class⟨\left(w{\cdot }_{𝑹}u\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right),\left(v{\cdot }_{𝑹}u\right){+}_{𝑹}\left(w{\cdot }_{𝑹}f\right)⟩$$
35	23 34	wceq	$$wffz=⟨\left(w{\cdot }_{𝑹}u\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right),\left(v{\cdot }_{𝑹}u\right){+}_{𝑹}\left(w{\cdot }_{𝑹}f\right)⟩$$
36	22 35	wa	$$wff\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨\left(w{\cdot }_{𝑹}u\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right),\left(v{\cdot }_{𝑹}u\right){+}_{𝑹}\left(w{\cdot }_{𝑹}f\right)⟩\right)$$
37	36 13	wex	$$wff\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨\left(w{\cdot }_{𝑹}u\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right),\left(v{\cdot }_{𝑹}u\right){+}_{𝑹}\left(w{\cdot }_{𝑹}f\right)⟩\right)$$
38	37 12	wex	$$wff\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨\left(w{\cdot }_{𝑹}u\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right),\left(v{\cdot }_{𝑹}u\right){+}_{𝑹}\left(w{\cdot }_{𝑹}f\right)⟩\right)$$
39	38 11	wex	$$wff\exists v\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨\left(w{\cdot }_{𝑹}u\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right),\left(v{\cdot }_{𝑹}u\right){+}_{𝑹}\left(w{\cdot }_{𝑹}f\right)⟩\right)$$
40	39 10	wex	$$wff\exists w\exists v\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨\left(w{\cdot }_{𝑹}u\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right),\left(v{\cdot }_{𝑹}u\right){+}_{𝑹}\left(w{\cdot }_{𝑹}f\right)⟩\right)$$
41	9 40	wa	$$wff\left(\left(x\in ℂ\wedge y\in ℂ\right)\wedge \exists w\exists v\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨\left(w{\cdot }_{𝑹}u\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right),\left(v{\cdot }_{𝑹}u\right){+}_{𝑹}\left(w{\cdot }_{𝑹}f\right)⟩\right)\right)$$
42	41 1 2 3	coprab	$$class\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in ℂ\wedge y\in ℂ\right)\wedge \exists w\exists v\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨\left(w{\cdot }_{𝑹}u\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right),\left(v{\cdot }_{𝑹}u\right){+}_{𝑹}\left(w{\cdot }_{𝑹}f\right)⟩\right)\right)\right\}$$
43	0 42	wceq	$$wff\times =\left\{⟨⟨x,y⟩,z⟩|\left(\left(x\in ℂ\wedge y\in ℂ\right)\wedge \exists w\exists v\exists u\exists f\left(\left(x=⟨w,v⟩\wedge y=⟨u,f⟩\right)\wedge z=⟨\left(w{\cdot }_{𝑹}u\right){+}_{𝑹}\left({-1}_{𝑹}{\cdot }_{𝑹}\left(v{\cdot }_{𝑹}f\right)\right),\left(v{\cdot }_{𝑹}u\right){+}_{𝑹}\left(w{\cdot }_{𝑹}f\right)⟩\right)\right)\right\}$$