df-muls

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

		Ref	Expression
	Assertion	df-muls	$⊢ \cdot_{s} = {norec2}_{s} #A# ((z \in V, m \in V ⟼ ⦋ 1^{st} (z) / x ⦌ ⦋ 2^{nd} (z) / y ⦌ ((\{a \| \exists p \in L (x) \exists q \in L (y) a = ((p m y) +_{s} (x m q)) -_{s} (p m q)\} \cup \{b \| \exists r \in R (x) \exists s \in R (y) b = ((r m y) +_{s} (x m s)) -_{s} (r m s)\}) \|_{s} (\{c \| \exists t \in L (x) \exists u \in R (y) c = ((t m y) +_{s} (x m u)) -_{s} (t m u)\} \cup \{d \| \exists v \in R (x) \exists w \in L (y) d = ((v m y) +_{s} (x m w)) -_{s} (v m w)\}))))$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-muls

Detailed syntax breakdown