Metamath Proof Explorer

Definition df-mul

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

Ref Expression
Assertion 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 ) ) >. ) ) }

Detailed syntax breakdown

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