Definition df-mul 5258

Description: Define multiplication over complex numbers.

Assertion

Ref	Expression
df-mul	|- x. = {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))}

Distinct variable group:   x,y,z,w,v,u,f

Detailed syntax breakdown of Definition df-mul

Step	Hyp	Ref	Expression
1		cmul 5251	. 2 class x.
2		vx	. . . . . . 7 set x
3	2	cv 957	. . . . . 6 class x
4		cc 5244	. . . . . 6 class CC
5	3, 4	wcel 960	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 set y
7	6	cv 957	. . . . . 6 class y
8	7, 4	wcel 960	. . . . 5 wff y e. CC
9	5, 8	wa 223	. . . 4 wff (x e. CC /\ y e. CC)
10		vw	. . . . . . . . . . . . 13 set w
11	10	cv 957	. . . . . . . . . . . 12 class w
12		vv	. . . . . . . . . . . . 13 set v
13	12	cv 957	. . . . . . . . . . . 12 class v
14	11, 13	cop 2415	. . . . . . . . . . 11 class <.w, v>.
15	3, 14	wceq 958	. . . . . . . . . 10 wff x = <.w, v>.
16		vu	. . . . . . . . . . . . 13 set u
17	16	cv 957	. . . . . . . . . . . 12 class u
18		vf	. . . . . . . . . . . . 13 set f
19	18	cv 957	. . . . . . . . . . . 12 class f
20	17, 19	cop 2415	. . . . . . . . . . 11 class <.u, f>.
21	7, 20	wceq 958	. . . . . . . . . 10 wff y = <.u, f>.
22	15, 21	wa 223	. . . . . . . . 9 wff (x = <.w, v>. /\ y = <.u, f>.)
23		vz	. . . . . . . . . . 11 set z
24	23	cv 957	. . . . . . . . . 10 class z
25		cmr 5010	. . . . . . . . . . . . 13 class .R
26	11, 17, 25	co 3969	. . . . . . . . . . . 12 class (w .R u)
27		cm1r 5008	. . . . . . . . . . . . 13 class -1R
28	13, 19, 25	co 3969	. . . . . . . . . . . . 13 class (v .R f)
29	27, 28, 25	co 3969	. . . . . . . . . . . 12 class (-1R .R (v .R f))
30		cplr 5009	. . . . . . . . . . . 12 class +R
31	26, 29, 30	co 3969	. . . . . . . . . . 11 class ((w .R u) +R (-1R .R (v .R f)))
32	13, 17, 25	co 3969	. . . . . . . . . . . 12 class (v .R u)
33	11, 19, 25	co 3969	. . . . . . . . . . . 12 class (w .R f)
34	32, 33, 30	co 3969	. . . . . . . . . . 11 class ((v .R u) +R (w .R f))
35	31, 34	cop 2415	. . . . . . . . . 10 class <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.
36	24, 35	wceq 958	. . . . . . . . 9 wff z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.
37	22, 36	wa 223	. . . . . . . 8 wff ((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)
38	37, 18	wex 982	. . . . . . 7 wff E.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)
39	38, 16	wex 982	. . . . . 6 wff E.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)
40	39, 12	wex 982	. . . . 5 wff E.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)
41	40, 10	wex 982	. . . 4 wff E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.)
42	9, 41	wa 223	. . 3 wff ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))
43	42, 2, 6, 23	copab2 3970	. 2 class {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))}
44	1, 43	wceq 958	1 wff x. = {<.<.x, y>., z>. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w, v>. /\ y = <.u, f>.) /\ z = <.((w .R u) +R (-1R .R (v .R f))), ((v .R u) +R (w .R f))>.))}

This definition is referenced by:  mulcnsr 5266  axmulopr 5278

Copyright terms: Public domain