Metamath Proof Explorer

Definition df-mr

Description: Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c , and is intended to be used only by the construction. From Proposition 9-4.3 of Gleason p. 126. (Contributed by NM, 25-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion df-mr 
|- .R = { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R ) ) }

Detailed syntax breakdown

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