Metamath Proof Explorer

Definition df-muls

Description: Define surreal multiplication. Definition from Conway p. 5. (Contributed by Scott Fenton, 4-Feb-2025)

Ref Expression
Assertion df-muls 
|- x.s = norec2 ( ( z e. _V , m e. _V |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) } ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmuls 
 |-  x.s
1 vz 
 |-  z
2 cvv 
 |-  _V
3 vm 
 |-  m
4 c1st 
 |-  1st
5 1 cv 
 |-  z
6 5 4 cfv 
 |-  ( 1st ` z )
7 vx 
 |-  x
8 c2nd 
 |-  2nd
9 5 8 cfv 
 |-  ( 2nd ` z )
10 vy 
 |-  y
11 va 
 |-  a
12 vp 
 |-  p
13 cleft 
 |-  _Left
14 7 cv 
 |-  x
15 14 13 cfv 
 |-  ( _Left ` x )
16 vq 
 |-  q
17 10 cv 
 |-  y
18 17 13 cfv 
 |-  ( _Left ` y )
19 11 cv 
 |-  a
20 12 cv 
 |-  p
21 3 cv 
 |-  m
22 20 17 21 co 
 |-  ( p m y )
23 cadds 
 |-  +s
24 16 cv 
 |-  q
25 14 24 21 co 
 |-  ( x m q )
26 22 25 23 co 
 |-  ( ( p m y ) +s ( x m q ) )
27 csubs 
 |-  -s
28 20 24 21 co 
 |-  ( p m q )
29 26 28 27 co 
 |-  ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) )
30 19 29 wceq 
 |-  a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) )
31 30 16 18 wrex 
 |-  E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) )
32 31 12 15 wrex 
 |-  E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) )
33 32 11 cab 
 |-  { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) }
34 vb 
 |-  b
35 vr 
 |-  r
36 cright 
 |-  _Right
37 14 36 cfv 
 |-  ( _Right ` x )
38 vs 
 |-  s
39 17 36 cfv 
 |-  ( _Right ` y )
40 34 cv 
 |-  b
41 35 cv 
 |-  r
42 41 17 21 co 
 |-  ( r m y )
43 38 cv 
 |-  s
44 14 43 21 co 
 |-  ( x m s )
45 42 44 23 co 
 |-  ( ( r m y ) +s ( x m s ) )
46 41 43 21 co 
 |-  ( r m s )
47 45 46 27 co 
 |-  ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) )
48 40 47 wceq 
 |-  b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) )
49 48 38 39 wrex 
 |-  E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) )
50 49 35 37 wrex 
 |-  E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) )
51 50 34 cab 
 |-  { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) }
52 33 51 cun 
 |-  ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) } )
53 cscut 
 |-  |s
54 vc 
 |-  c
55 vt 
 |-  t
56 vu 
 |-  u
57 54 cv 
 |-  c
58 55 cv 
 |-  t
59 58 17 21 co 
 |-  ( t m y )
60 56 cv 
 |-  u
61 14 60 21 co 
 |-  ( x m u )
62 59 61 23 co 
 |-  ( ( t m y ) +s ( x m u ) )
63 58 60 21 co 
 |-  ( t m u )
64 62 63 27 co 
 |-  ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) )
65 57 64 wceq 
 |-  c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) )
66 65 56 39 wrex 
 |-  E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) )
67 66 55 15 wrex 
 |-  E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) )
68 67 54 cab 
 |-  { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) }
69 vd 
 |-  d
70 vv 
 |-  v
71 vw 
 |-  w
72 69 cv 
 |-  d
73 70 cv 
 |-  v
74 73 17 21 co 
 |-  ( v m y )
75 71 cv 
 |-  w
76 14 75 21 co 
 |-  ( x m w )
77 74 76 23 co 
 |-  ( ( v m y ) +s ( x m w ) )
78 73 75 21 co 
 |-  ( v m w )
79 77 78 27 co 
 |-  ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) )
80 72 79 wceq 
 |-  d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) )
81 80 71 18 wrex 
 |-  E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) )
82 81 70 37 wrex 
 |-  E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) )
83 82 69 cab 
 |-  { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) }
84 68 83 cun 
 |-  ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) } )
85 52 84 53 co 
 |-  ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) } ) )
86 10 9 85 csb 
 |-  [_ ( 2nd ` z ) / y ]_ ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) } ) )
87 7 6 86 csb 
 |-  [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) } ) )
88 1 3 2 2 87 cmpo 
 |-  ( z e. _V , m e. _V |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) } ) ) )
89 88 cnorec2 
 |-  norec2 ( ( z e. _V , m e. _V |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) } ) ) ) )
90 0 89 wceq 
 |-  x.s = norec2 ( ( z e. _V , m e. _V |-> [_ ( 1st ` z ) / x ]_ [_ ( 2nd ` z ) / y ]_ ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) } ) ) ) )