Definition df-muls

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

	Ref	Expression
Assertion	df-muls	Could not format assertion : No typesetting found for |- 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 ) ) } ) ) ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmuls	Could not format x.s : No typesetting found for class x.s with typecode class
1		vz	$$setvarz$$
2		cvv	$$class\mathrm{V}$$
3		vm	$$setvarm$$
4		c1st	$$class{1}^{st}$$
5	1	cv	$$setvarz$$
6	5 4	cfv	$$class{1}^{st}\left(z\right)$$
7		vx	$$setvarx$$
8		c2nd	$$class{2}^{nd}$$
9	5 8	cfv	$$class{2}^{nd}\left(z\right)$$
10		vy	$$setvary$$
11		va	$$setvara$$
12		vp	$$setvarp$$
13		cleft	Could not format _Left : No typesetting found for class _Left with typecode class
14	7	cv	$$setvarx$$
15	14 13	cfv	Could not format ( _Left ` x ) : No typesetting found for class ( _Left ` x ) with typecode class
16		vq	$$setvarq$$
17	10	cv	$$setvary$$
18	17 13	cfv	Could not format ( _Left ` y ) : No typesetting found for class ( _Left ` y ) with typecode class
19	11	cv	$$setvara$$
20	12	cv	$$setvarp$$
21	3	cv	$$setvarm$$
22	20 17 21	co	$$class\left(pmy\right)$$
23		cadds	Could not format +s : No typesetting found for class +s with typecode class
24	16	cv	$$setvarq$$
25	14 24 21	co	$$class\left(xmq\right)$$
26	22 25 23	co	Could not format ( ( p m y ) +s ( x m q ) ) : No typesetting found for class ( ( p m y ) +s ( x m q ) ) with typecode class
27		csubs	Could not format -s : No typesetting found for class -s with typecode class
28	20 24 21	co	$$class\left(pmq\right)$$
29	26 28 27	co	Could not format ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) : No typesetting found for class ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) with typecode class
30	19 29	wceq	Could not format a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) : No typesetting found for wff a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) with typecode wff
31	30 16 18	wrex	Could not format E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) : No typesetting found for wff E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) with typecode wff
32	31 12 15	wrex	Could not format E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) : No typesetting found for wff E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) with typecode wff
33	32 11	cab	Could not format { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) } : No typesetting found for class { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` y ) a = ( ( ( p m y ) +s ( x m q ) ) -s ( p m q ) ) } with typecode class
34		vb	$$setvarb$$
35		vr	$$setvarr$$
36		cright	Could not format _Right : No typesetting found for class _Right with typecode class
37	14 36	cfv	Could not format ( _Right ` x ) : No typesetting found for class ( _Right ` x ) with typecode class
38		vs	$$setvars$$
39	17 36	cfv	Could not format ( _Right ` y ) : No typesetting found for class ( _Right ` y ) with typecode class
40	34	cv	$$setvarb$$
41	35	cv	$$setvarr$$
42	41 17 21	co	$$class\left(rmy\right)$$
43	38	cv	$$setvars$$
44	14 43 21	co	$$class\left(xms\right)$$
45	42 44 23	co	Could not format ( ( r m y ) +s ( x m s ) ) : No typesetting found for class ( ( r m y ) +s ( x m s ) ) with typecode class
46	41 43 21	co	$$class\left(rms\right)$$
47	45 46 27	co	Could not format ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) : No typesetting found for class ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) with typecode class
48	40 47	wceq	Could not format b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) : No typesetting found for wff b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) with typecode wff
49	48 38 39	wrex	Could not format E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) : No typesetting found for wff E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) with typecode wff
50	49 35 37	wrex	Could not format E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) : No typesetting found for wff E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) with typecode wff
51	50 34	cab	Could not format { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) } : No typesetting found for class { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` y ) b = ( ( ( r m y ) +s ( x m s ) ) -s ( r m s ) ) } with typecode class
52	33 51	cun	Could not format ( { 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 ) ) } ) : No typesetting found for class ( { 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 ) ) } ) with typecode class
53		cscut	$$class{|}_s$$
54		vc	$$setvarc$$
55		vt	$$setvart$$
56		vu	$$setvaru$$
57	54	cv	$$setvarc$$
58	55	cv	$$setvart$$
59	58 17 21	co	$$class\left(tmy\right)$$
60	56	cv	$$setvaru$$
61	14 60 21	co	$$class\left(xmu\right)$$
62	59 61 23	co	Could not format ( ( t m y ) +s ( x m u ) ) : No typesetting found for class ( ( t m y ) +s ( x m u ) ) with typecode class
63	58 60 21	co	$$class\left(tmu\right)$$
64	62 63 27	co	Could not format ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) : No typesetting found for class ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) with typecode class
65	57 64	wceq	Could not format c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) : No typesetting found for wff c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) with typecode wff
66	65 56 39	wrex	Could not format E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) : No typesetting found for wff E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) with typecode wff
67	66 55 15	wrex	Could not format E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) : No typesetting found for wff E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) with typecode wff
68	67 54	cab	Could not format { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) } : No typesetting found for class { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` y ) c = ( ( ( t m y ) +s ( x m u ) ) -s ( t m u ) ) } with typecode class
69		vd	$$setvard$$
70		vv	$$setvarv$$
71		vw	$$setvarw$$
72	69	cv	$$setvard$$
73	70	cv	$$setvarv$$
74	73 17 21	co	$$class\left(vmy\right)$$
75	71	cv	$$setvarw$$
76	14 75 21	co	$$class\left(xmw\right)$$
77	74 76 23	co	Could not format ( ( v m y ) +s ( x m w ) ) : No typesetting found for class ( ( v m y ) +s ( x m w ) ) with typecode class
78	73 75 21	co	$$class\left(vmw\right)$$
79	77 78 27	co	Could not format ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) : No typesetting found for class ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) with typecode class
80	72 79	wceq	Could not format d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) : No typesetting found for wff d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) with typecode wff
81	80 71 18	wrex	Could not format E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) : No typesetting found for wff E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) with typecode wff
82	81 70 37	wrex	Could not format E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) : No typesetting found for wff E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) with typecode wff
83	82 69	cab	Could not format { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) } : No typesetting found for class { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` y ) d = ( ( ( v m y ) +s ( x m w ) ) -s ( v m w ) ) } with typecode class
84	68 83	cun	Could not format ( { 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 ) ) } ) : No typesetting found for class ( { 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 ) ) } ) with typecode class
85	52 84 53	co	Could not format ( ( { 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 ) ) } ) ) : No typesetting found for class ( ( { 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 ) ) } ) ) with typecode class
86	10 9 85	csb	Could not format [_ ( 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 ) ) } ) ) : No typesetting found for class [_ ( 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 ) ) } ) ) with typecode class
87	7 6 86	csb	Could not format [_ ( 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 ) ) } ) ) : No typesetting found for class [_ ( 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 ) ) } ) ) with typecode class
88	1 3 2 2 87	cmpo	Could not format ( 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 ) ) } ) ) ) : No typesetting found for class ( 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 ) ) } ) ) ) with typecode class
89	88	cnorec2	Could not format 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 ) ) } ) ) ) ) : No typesetting found for class 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 ) ) } ) ) ) ) with typecode class
90	0 89	wceq	Could not format 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 ) ) } ) ) ) ) : No typesetting found for wff 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 ) ) } ) ) ) ) with typecode wff