Definition df-mul 7823

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

Assertion

Ref	Expression
df-mul	|- x. = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u 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 ) ) >. ) ) }

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

Detailed syntax breakdown of Definition df-mul

Step	Hyp	Ref	Expression
1		cmul 7816	. 2 class x.
2		vx	. . . . . . 7 setvar x
3	2	cv 1352	. . . . . 6 class x
4		cc 7809	. . . . . 6 class CC
5	3, 4	wcel 2148	. . . . 5 wff x e. CC
6		vy	. . . . . . 7 setvar y
7	6	cv 1352	. . . . . 6 class y
8	7, 4	wcel 2148	. . . . 5 wff y e. CC
9	5, 8	wa 104	. . . 4 wff ( x e. CC /\ y e. CC )
10		vw	. . . . . . . . . . . . 13 setvar w
11	10	cv 1352	. . . . . . . . . . . 12 class w
12		vv	. . . . . . . . . . . . 13 setvar v
13	12	cv 1352	. . . . . . . . . . . 12 class v
14	11, 13	cop 3596	. . . . . . . . . . 11 class <. w , v >.
15	3, 14	wceq 1353	. . . . . . . . . 10 wff x = <. w , v >.
16		vu	. . . . . . . . . . . . 13 setvar u
17	16	cv 1352	. . . . . . . . . . . 12 class u
18		vf	. . . . . . . . . . . . 13 setvar f
19	18	cv 1352	. . . . . . . . . . . 12 class f
20	17, 19	cop 3596	. . . . . . . . . . 11 class <. u , f >.
21	7, 20	wceq 1353	. . . . . . . . . 10 wff y = <. u , f >.
22	15, 21	wa 104	. . . . . . . . 9 wff ( x = <. w , v >. /\ y = <. u , f >. )
23		vz	. . . . . . . . . . 11 setvar z
24	23	cv 1352	. . . . . . . . . 10 class z
25		cmr 7301	. . . . . . . . . . . . 13 class .R
26	11, 17, 25	co 5875	. . . . . . . . . . . 12 class ( w .R u )
27		cm1r 7299	. . . . . . . . . . . . 13 class -1R
28	13, 19, 25	co 5875	. . . . . . . . . . . . 13 class ( v .R f )
29	27, 28, 25	co 5875	. . . . . . . . . . . 12 class ( -1R .R ( v .R f ) )
30		cplr 7300	. . . . . . . . . . . 12 class +R
31	26, 29, 30	co 5875	. . . . . . . . . . 11 class ( ( w .R u ) +R ( -1R .R ( v .R f ) ) )
32	13, 17, 25	co 5875	. . . . . . . . . . . 12 class ( v .R u )
33	11, 19, 25	co 5875	. . . . . . . . . . . 12 class ( w .R f )
34	32, 33, 30	co 5875	. . . . . . . . . . 11 class ( ( v .R u ) +R ( w .R f ) )
35	31, 34	cop 3596	. . . . . . . . . 10 class <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >.
36	24, 35	wceq 1353	. . . . . . . . 9 wff z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >.
37	22, 36	wa 104	. . . . . . . 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 1492	. . . . . . 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 1492	. . . . . 6 wff E. u 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 ) ) >. )
40	39, 12	wex 1492	. . . . 5 wff E. v E. u 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 ) ) >. )
41	40, 10	wex 1492	. . . 4 wff E. w E. v E. u 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 ) ) >. )
42	9, 41	wa 104	. . 3 wff ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u 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 ) ) >. ) )
43	42, 2, 6, 23	coprab 5876	. 2 class { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u 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 ) ) >. ) ) }
44	1, 43	wceq 1353	1 wff x. = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u 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 ) ) >. ) ) }

This definition is referenced by:  mulcnsr  7834  axmulf  7868