Definition df-muls 27543

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

Assertion

Ref	Expression
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 (𝑣𝑚𝑤))}))))

Distinct variable group:   𝑧,𝑚,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑟,𝑠,𝑡,𝑢,𝑣,𝑤,𝑥,𝑦

Detailed syntax breakdown of Definition df-muls

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

This definition is referenced by:  mulsfn  27544  mulsval  27545