Metamath Proof Explorer

Definition df-adds

Description: Define surreal addition. This is the first of the field operations on the surreals. Definition from Conway p. 5. Definition from Gonshor p. 13. (Contributed by Scott Fenton, 20-Aug-2024)

Ref Expression
Assertion df-adds 
|- +s = norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cadds 
 |-  +s
1 vx 
 |-  x
2 cvv 
 |-  _V
3 va 
 |-  a
4 vy 
 |-  y
5 vl 
 |-  l
6 cleft 
 |-  _L
7 c1st 
 |-  1st
8 1 cv 
 |-  x
9 8 7 cfv 
 |-  ( 1st ` x )
10 9 6 cfv 
 |-  ( _L ` ( 1st ` x ) )
11 4 cv 
 |-  y
12 5 cv 
 |-  l
13 3 cv 
 |-  a
14 c2nd 
 |-  2nd
15 8 14 cfv 
 |-  ( 2nd ` x )
16 12 15 13 co 
 |-  ( l a ( 2nd ` x ) )
17 11 16 wceq 
 |-  y = ( l a ( 2nd ` x ) )
18 17 5 10 wrex 
 |-  E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) )
19 18 4 cab 
 |-  { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) }
20 vz 
 |-  z
21 15 6 cfv 
 |-  ( _L ` ( 2nd ` x ) )
22 20 cv 
 |-  z
23 9 12 13 co 
 |-  ( ( 1st ` x ) a l )
24 22 23 wceq 
 |-  z = ( ( 1st ` x ) a l )
25 24 5 21 wrex 
 |-  E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l )
26 25 20 cab 
 |-  { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) }
27 19 26 cun 
 |-  ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } )
28 cscut 
 |-  |s
29 vr 
 |-  r
30 cright 
 |-  _R
31 9 30 cfv 
 |-  ( _R ` ( 1st ` x ) )
32 29 cv 
 |-  r
33 32 15 13 co 
 |-  ( r a ( 2nd ` x ) )
34 11 33 wceq 
 |-  y = ( r a ( 2nd ` x ) )
35 34 29 31 wrex 
 |-  E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) )
36 35 4 cab 
 |-  { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) }
37 15 30 cfv 
 |-  ( _R ` ( 2nd ` x ) )
38 9 32 13 co 
 |-  ( ( 1st ` x ) a r )
39 22 38 wceq 
 |-  z = ( ( 1st ` x ) a r )
40 39 29 37 wrex 
 |-  E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r )
41 40 20 cab 
 |-  { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) }
42 36 41 cun 
 |-  ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } )
43 27 42 28 co 
 |-  ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) )
44 1 3 2 2 43 cmpo 
 |-  ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) )
45 44 cnorec2 
 |-  norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) )
46 0 45 wceq 
 |-  +s = norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) )