Definition df-muls

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

	Ref	Expression
Assertion	df-muls	⊢ ·s = norec2 ( ( 𝑧 ∈ V , 𝑚 ∈ V ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) ) } ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmuls	⊢ ·s
1		vz	⊢ 𝑧
2		cvv	⊢ V
3		vm	⊢ 𝑚
4		c1st	⊢ 1st
5	1	cv	⊢ 𝑧
6	5 4	cfv	⊢ ( 1st ‘ 𝑧 )
7		vx	⊢ 𝑥
8		c2nd	⊢ 2nd
9	5 8	cfv	⊢ ( 2nd ‘ 𝑧 )
10		vy	⊢ 𝑦
11		va	⊢ 𝑎
12		vp	⊢ 𝑝
13		cleft	⊢ L
14	7	cv	⊢ 𝑥
15	14 13	cfv	⊢ ( L ‘ 𝑥 )
16		vq	⊢ 𝑞
17	10	cv	⊢ 𝑦
18	17 13	cfv	⊢ ( L ‘ 𝑦 )
19	11	cv	⊢ 𝑎
20	12	cv	⊢ 𝑝
21	3	cv	⊢ 𝑚
22	20 17 21	co	⊢ ( 𝑝 𝑚 𝑦 )
23		cadds	⊢ +s
24	16	cv	⊢ 𝑞
25	14 24 21	co	⊢ ( 𝑥 𝑚 𝑞 )
26	22 25 23	co	⊢ ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) )
27		csubs	⊢ -s
28	20 24 21	co	⊢ ( 𝑝 𝑚 𝑞 )
29	26 28 27	co	⊢ ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) )
30	19 29	wceq	⊢ 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) )
31	30 16 18	wrex	⊢ ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) )
32	31 12 15	wrex	⊢ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) )
33	32 11	cab	⊢ { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) ) }
34		vb	⊢ 𝑏
35		vr	⊢ 𝑟
36		cright	⊢ R
37	14 36	cfv	⊢ ( R ‘ 𝑥 )
38		vs	⊢ 𝑠
39	17 36	cfv	⊢ ( R ‘ 𝑦 )
40	34	cv	⊢ 𝑏
41	35	cv	⊢ 𝑟
42	41 17 21	co	⊢ ( 𝑟 𝑚 𝑦 )
43	38	cv	⊢ 𝑠
44	14 43 21	co	⊢ ( 𝑥 𝑚 𝑠 )
45	42 44 23	co	⊢ ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) )
46	41 43 21	co	⊢ ( 𝑟 𝑚 𝑠 )
47	45 46 27	co	⊢ ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) )
48	40 47	wceq	⊢ 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) )
49	48 38 39	wrex	⊢ ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) )
50	49 35 37	wrex	⊢ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) )
51	50 34	cab	⊢ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) ) }
52	33 51	cun	⊢ ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) ) } )
53		ccuts	⊢ |s
54		vc	⊢ 𝑐
55		vt	⊢ 𝑡
56		vu	⊢ 𝑢
57	54	cv	⊢ 𝑐
58	55	cv	⊢ 𝑡
59	58 17 21	co	⊢ ( 𝑡 𝑚 𝑦 )
60	56	cv	⊢ 𝑢
61	14 60 21	co	⊢ ( 𝑥 𝑚 𝑢 )
62	59 61 23	co	⊢ ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) )
63	58 60 21	co	⊢ ( 𝑡 𝑚 𝑢 )
64	62 63 27	co	⊢ ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) )
65	57 64	wceq	⊢ 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) )
66	65 56 39	wrex	⊢ ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) )
67	66 55 15	wrex	⊢ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) )
68	67 54	cab	⊢ { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) ) }
69		vd	⊢ 𝑑
70		vv	⊢ 𝑣
71		vw	⊢ 𝑤
72	69	cv	⊢ 𝑑
73	70	cv	⊢ 𝑣
74	73 17 21	co	⊢ ( 𝑣 𝑚 𝑦 )
75	71	cv	⊢ 𝑤
76	14 75 21	co	⊢ ( 𝑥 𝑚 𝑤 )
77	74 76 23	co	⊢ ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) )
78	73 75 21	co	⊢ ( 𝑣 𝑚 𝑤 )
79	77 78 27	co	⊢ ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) )
80	72 79	wceq	⊢ 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) )
81	80 71 18	wrex	⊢ ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) )
82	81 70 37	wrex	⊢ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) )
83	82 69	cab	⊢ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) ) }
84	68 83	cun	⊢ ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) ) } )
85	52 84 53	co	⊢ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) ) } ) )
86	10 9 85	csb	⊢ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) ) } ) )
87	7 6 86	csb	⊢ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) ) } ) )
88	1 3 2 2 87	cmpo	⊢ ( 𝑧 ∈ V , 𝑚 ∈ V ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) ) } ) ) )
89	88	cnorec2	⊢ norec2 ( ( 𝑧 ∈ V , 𝑚 ∈ V ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) ) } ) ) ) )
90	0 89	wceq	⊢ ·s = norec2 ( ( 𝑧 ∈ V , 𝑚 ∈ V ↦ ⦋ ( 1st ‘ 𝑧 ) / 𝑥 ⦌ ⦋ ( 2nd ‘ 𝑧 ) / 𝑦 ⦌ ( ( { 𝑎 ∣ ∃ 𝑝 ∈ ( L ‘ 𝑥 ) ∃ 𝑞 ∈ ( L ‘ 𝑦 ) 𝑎 = ( ( ( 𝑝 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑞 ) ) -s ( 𝑝 𝑚 𝑞 ) ) } ∪ { 𝑏 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑥 ) ∃ 𝑠 ∈ ( R ‘ 𝑦 ) 𝑏 = ( ( ( 𝑟 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑠 ) ) -s ( 𝑟 𝑚 𝑠 ) ) } ) |s ( { 𝑐 ∣ ∃ 𝑡 ∈ ( L ‘ 𝑥 ) ∃ 𝑢 ∈ ( R ‘ 𝑦 ) 𝑐 = ( ( ( 𝑡 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑢 ) ) -s ( 𝑡 𝑚 𝑢 ) ) } ∪ { 𝑑 ∣ ∃ 𝑣 ∈ ( R ‘ 𝑥 ) ∃ 𝑤 ∈ ( L ‘ 𝑦 ) 𝑑 = ( ( ( 𝑣 𝑚 𝑦 ) +s ( 𝑥 𝑚 𝑤 ) ) -s ( 𝑣 𝑚 𝑤 ) ) } ) ) ) )