mulsunif2

Description: Alternate expression for surreal multiplication. Note from Conway p. 19. (Contributed by Scott Fenton, 16-Mar-2025)

	Ref	Expression
Hypotheses	mulsunif2.1	$⊢ φ \to L ≪_{s} R$
	mulsunif2.2	$⊢ φ \to M ≪_{s} S$
	mulsunif2.3	$⊢ φ \to A = L \|_{s} R$
	mulsunif2.4	$⊢ φ \to B = M \|_{s} S$
Assertion	mulsunif2	$⊢ φ \to A \cdot_{s} B = (\{a \| \exists p \in L \exists q \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q))\} \cup \{b \| \exists r \in R \exists s \in S b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B))\}) \|_{s} (\{c \| \exists t \in L \exists u \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B))\} \cup \{d \| \exists v \in R \exists w \in M d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w))\})$

Proof

Step	Hyp	Ref	Expression
1		mulsunif2.1	$⊢ φ \to L ≪_{s} R$
2		mulsunif2.2	$⊢ φ \to M ≪_{s} S$
3		mulsunif2.3	$⊢ φ \to A = L \|_{s} R$
4		mulsunif2.4	$⊢ φ \to B = M \|_{s} S$
5	1 2 3 4	mulsunif2lem	$⊢ φ \to A \cdot_{s} B = (\{e \| \exists i \in L \exists j \in M e = (A \cdot_{s} B) -_{s} ((A -_{s} i) \cdot_{s} (B -_{s} j))\} \cup \{f \| \exists k \in R \exists l \in S f = (A \cdot_{s} B) -_{s} ((k -_{s} A) \cdot_{s} (l -_{s} B))\}) \|_{s} (\{g \| \exists m \in L \exists n \in S g = (A \cdot_{s} B) +_{s} ((A -_{s} m) \cdot_{s} (n -_{s} B))\} \cup \{h \| \exists o \in R \exists x \in M h = (A \cdot_{s} B) +_{s} ((o -_{s} A) \cdot_{s} (B -_{s} x))\})$
6		eqeq1	$⊢ e = a \to (e = (A \cdot_{s} B) -_{s} ((A -_{s} i) \cdot_{s} (B -_{s} j)) \leftrightarrow a = (A \cdot_{s} B) -_{s} ((A -_{s} i) \cdot_{s} (B -_{s} j)))$
7	6	2rexbidv	$⊢ e = a \to (\exists i \in L \exists j \in M e = (A \cdot_{s} B) -_{s} ((A -_{s} i) \cdot_{s} (B -_{s} j)) \leftrightarrow \exists i \in L \exists j \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} i) \cdot_{s} (B -_{s} j)))$
8		oveq2	$⊢ i = p \to A -_{s} i = A -_{s} p$
9	8	oveq1d	$⊢ i = p \to (A -_{s} i) \cdot_{s} (B -_{s} j) = (A -_{s} p) \cdot_{s} (B -_{s} j)$
10	9	oveq2d	$⊢ i = p \to (A \cdot_{s} B) -_{s} ((A -_{s} i) \cdot_{s} (B -_{s} j)) = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} j))$
11	10	eqeq2d	$⊢ i = p \to (a = (A \cdot_{s} B) -_{s} ((A -_{s} i) \cdot_{s} (B -_{s} j)) \leftrightarrow a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} j)))$
12		oveq2	$⊢ j = q \to B -_{s} j = B -_{s} q$
13	12	oveq2d	$⊢ j = q \to (A -_{s} p) \cdot_{s} (B -_{s} j) = (A -_{s} p) \cdot_{s} (B -_{s} q)$
14	13	oveq2d	$⊢ j = q \to (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} j)) = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q))$
15	14	eqeq2d	$⊢ j = q \to (a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} j)) \leftrightarrow a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q)))$
16	11 15	cbvrex2vw	$⊢ \exists i \in L \exists j \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} i) \cdot_{s} (B -_{s} j)) \leftrightarrow \exists p \in L \exists q \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q))$
17	7 16	bitrdi	$⊢ e = a \to (\exists i \in L \exists j \in M e = (A \cdot_{s} B) -_{s} ((A -_{s} i) \cdot_{s} (B -_{s} j)) \leftrightarrow \exists p \in L \exists q \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q)))$
18	17	cbvabv	$⊢ \{e \| \exists i \in L \exists j \in M e = (A \cdot_{s} B) -_{s} ((A -_{s} i) \cdot_{s} (B -_{s} j))\} = \{a \| \exists p \in L \exists q \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q))\}$
19		eqeq1	$⊢ f = b \to (f = (A \cdot_{s} B) -_{s} ((k -_{s} A) \cdot_{s} (l -_{s} B)) \leftrightarrow b = (A \cdot_{s} B) -_{s} ((k -_{s} A) \cdot_{s} (l -_{s} B)))$
20	19	2rexbidv	$⊢ f = b \to (\exists k \in R \exists l \in S f = (A \cdot_{s} B) -_{s} ((k -_{s} A) \cdot_{s} (l -_{s} B)) \leftrightarrow \exists k \in R \exists l \in S b = (A \cdot_{s} B) -_{s} ((k -_{s} A) \cdot_{s} (l -_{s} B)))$
21		oveq1	$⊢ k = r \to k -_{s} A = r -_{s} A$
22	21	oveq1d	$⊢ k = r \to (k -_{s} A) \cdot_{s} (l -_{s} B) = (r -_{s} A) \cdot_{s} (l -_{s} B)$
23	22	oveq2d	$⊢ k = r \to (A \cdot_{s} B) -_{s} ((k -_{s} A) \cdot_{s} (l -_{s} B)) = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (l -_{s} B))$
24	23	eqeq2d	$⊢ k = r \to (b = (A \cdot_{s} B) -_{s} ((k -_{s} A) \cdot_{s} (l -_{s} B)) \leftrightarrow b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (l -_{s} B)))$
25		oveq1	$⊢ l = s \to l -_{s} B = s -_{s} B$
26	25	oveq2d	$⊢ l = s \to (r -_{s} A) \cdot_{s} (l -_{s} B) = (r -_{s} A) \cdot_{s} (s -_{s} B)$
27	26	oveq2d	$⊢ l = s \to (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (l -_{s} B)) = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B))$
28	27	eqeq2d	$⊢ l = s \to (b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (l -_{s} B)) \leftrightarrow b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B)))$
29	24 28	cbvrex2vw	$⊢ \exists k \in R \exists l \in S b = (A \cdot_{s} B) -_{s} ((k -_{s} A) \cdot_{s} (l -_{s} B)) \leftrightarrow \exists r \in R \exists s \in S b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B))$
30	20 29	bitrdi	$⊢ f = b \to (\exists k \in R \exists l \in S f = (A \cdot_{s} B) -_{s} ((k -_{s} A) \cdot_{s} (l -_{s} B)) \leftrightarrow \exists r \in R \exists s \in S b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B)))$
31	30	cbvabv	$⊢ \{f \| \exists k \in R \exists l \in S f = (A \cdot_{s} B) -_{s} ((k -_{s} A) \cdot_{s} (l -_{s} B))\} = \{b \| \exists r \in R \exists s \in S b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B))\}$
32	18 31	uneq12i	$⊢ \{e \| \exists i \in L \exists j \in M e = (A \cdot_{s} B) -_{s} ((A -_{s} i) \cdot_{s} (B -_{s} j))\} \cup \{f \| \exists k \in R \exists l \in S f = (A \cdot_{s} B) -_{s} ((k -_{s} A) \cdot_{s} (l -_{s} B))\} = \{a \| \exists p \in L \exists q \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q))\} \cup \{b \| \exists r \in R \exists s \in S b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B))\}$
33		eqeq1	$⊢ g = c \to (g = (A \cdot_{s} B) +_{s} ((A -_{s} m) \cdot_{s} (n -_{s} B)) \leftrightarrow c = (A \cdot_{s} B) +_{s} ((A -_{s} m) \cdot_{s} (n -_{s} B)))$
34	33	2rexbidv	$⊢ g = c \to (\exists m \in L \exists n \in S g = (A \cdot_{s} B) +_{s} ((A -_{s} m) \cdot_{s} (n -_{s} B)) \leftrightarrow \exists m \in L \exists n \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} m) \cdot_{s} (n -_{s} B)))$
35		oveq2	$⊢ m = t \to A -_{s} m = A -_{s} t$
36	35	oveq1d	$⊢ m = t \to (A -_{s} m) \cdot_{s} (n -_{s} B) = (A -_{s} t) \cdot_{s} (n -_{s} B)$
37	36	oveq2d	$⊢ m = t \to (A \cdot_{s} B) +_{s} ((A -_{s} m) \cdot_{s} (n -_{s} B)) = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (n -_{s} B))$
38	37	eqeq2d	$⊢ m = t \to (c = (A \cdot_{s} B) +_{s} ((A -_{s} m) \cdot_{s} (n -_{s} B)) \leftrightarrow c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (n -_{s} B)))$
39		oveq1	$⊢ n = u \to n -_{s} B = u -_{s} B$
40	39	oveq2d	$⊢ n = u \to (A -_{s} t) \cdot_{s} (n -_{s} B) = (A -_{s} t) \cdot_{s} (u -_{s} B)$
41	40	oveq2d	$⊢ n = u \to (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (n -_{s} B)) = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B))$
42	41	eqeq2d	$⊢ n = u \to (c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (n -_{s} B)) \leftrightarrow c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B)))$
43	38 42	cbvrex2vw	$⊢ \exists m \in L \exists n \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} m) \cdot_{s} (n -_{s} B)) \leftrightarrow \exists t \in L \exists u \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B))$
44	34 43	bitrdi	$⊢ g = c \to (\exists m \in L \exists n \in S g = (A \cdot_{s} B) +_{s} ((A -_{s} m) \cdot_{s} (n -_{s} B)) \leftrightarrow \exists t \in L \exists u \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B)))$
45	44	cbvabv	$⊢ \{g \| \exists m \in L \exists n \in S g = (A \cdot_{s} B) +_{s} ((A -_{s} m) \cdot_{s} (n -_{s} B))\} = \{c \| \exists t \in L \exists u \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B))\}$
46		eqeq1	$⊢ h = d \to (h = (A \cdot_{s} B) +_{s} ((o -_{s} A) \cdot_{s} (B -_{s} x)) \leftrightarrow d = (A \cdot_{s} B) +_{s} ((o -_{s} A) \cdot_{s} (B -_{s} x)))$
47	46	2rexbidv	$⊢ h = d \to (\exists o \in R \exists x \in M h = (A \cdot_{s} B) +_{s} ((o -_{s} A) \cdot_{s} (B -_{s} x)) \leftrightarrow \exists o \in R \exists x \in M d = (A \cdot_{s} B) +_{s} ((o -_{s} A) \cdot_{s} (B -_{s} x)))$
48		oveq1	$⊢ o = v \to o -_{s} A = v -_{s} A$
49	48	oveq1d	$⊢ o = v \to (o -_{s} A) \cdot_{s} (B -_{s} x) = (v -_{s} A) \cdot_{s} (B -_{s} x)$
50	49	oveq2d	$⊢ o = v \to (A \cdot_{s} B) +_{s} ((o -_{s} A) \cdot_{s} (B -_{s} x)) = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} x))$
51	50	eqeq2d	$⊢ o = v \to (d = (A \cdot_{s} B) +_{s} ((o -_{s} A) \cdot_{s} (B -_{s} x)) \leftrightarrow d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} x)))$
52		oveq2	$⊢ x = w \to B -_{s} x = B -_{s} w$
53	52	oveq2d	$⊢ x = w \to (v -_{s} A) \cdot_{s} (B -_{s} x) = (v -_{s} A) \cdot_{s} (B -_{s} w)$
54	53	oveq2d	$⊢ x = w \to (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} x)) = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w))$
55	54	eqeq2d	$⊢ x = w \to (d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} x)) \leftrightarrow d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w)))$
56	51 55	cbvrex2vw	$⊢ \exists o \in R \exists x \in M d = (A \cdot_{s} B) +_{s} ((o -_{s} A) \cdot_{s} (B -_{s} x)) \leftrightarrow \exists v \in R \exists w \in M d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w))$
57	47 56	bitrdi	$⊢ h = d \to (\exists o \in R \exists x \in M h = (A \cdot_{s} B) +_{s} ((o -_{s} A) \cdot_{s} (B -_{s} x)) \leftrightarrow \exists v \in R \exists w \in M d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w)))$
58	57	cbvabv	$⊢ \{h \| \exists o \in R \exists x \in M h = (A \cdot_{s} B) +_{s} ((o -_{s} A) \cdot_{s} (B -_{s} x))\} = \{d \| \exists v \in R \exists w \in M d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w))\}$
59	45 58	uneq12i	$⊢ \{g \| \exists m \in L \exists n \in S g = (A \cdot_{s} B) +_{s} ((A -_{s} m) \cdot_{s} (n -_{s} B))\} \cup \{h \| \exists o \in R \exists x \in M h = (A \cdot_{s} B) +_{s} ((o -_{s} A) \cdot_{s} (B -_{s} x))\} = \{c \| \exists t \in L \exists u \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B))\} \cup \{d \| \exists v \in R \exists w \in M d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w))\}$
60	32 59	oveq12i	$⊢ (\{e \| \exists i \in L \exists j \in M e = (A \cdot_{s} B) -_{s} ((A -_{s} i) \cdot_{s} (B -_{s} j))\} \cup \{f \| \exists k \in R \exists l \in S f = (A \cdot_{s} B) -_{s} ((k -_{s} A) \cdot_{s} (l -_{s} B))\}) \|_{s} (\{g \| \exists m \in L \exists n \in S g = (A \cdot_{s} B) +_{s} ((A -_{s} m) \cdot_{s} (n -_{s} B))\} \cup \{h \| \exists o \in R \exists x \in M h = (A \cdot_{s} B) +_{s} ((o -_{s} A) \cdot_{s} (B -_{s} x))\}) = (\{a \| \exists p \in L \exists q \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q))\} \cup \{b \| \exists r \in R \exists s \in S b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B))\}) \|_{s} (\{c \| \exists t \in L \exists u \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B))\} \cup \{d \| \exists v \in R \exists w \in M d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w))\})$
61	5 60	eqtrdi	$⊢ φ \to A \cdot_{s} B = (\{a \| \exists p \in L \exists q \in M a = (A \cdot_{s} B) -_{s} ((A -_{s} p) \cdot_{s} (B -_{s} q))\} \cup \{b \| \exists r \in R \exists s \in S b = (A \cdot_{s} B) -_{s} ((r -_{s} A) \cdot_{s} (s -_{s} B))\}) \|_{s} (\{c \| \exists t \in L \exists u \in S c = (A \cdot_{s} B) +_{s} ((A -_{s} t) \cdot_{s} (u -_{s} B))\} \cup \{d \| \exists v \in R \exists w \in M d = (A \cdot_{s} B) +_{s} ((v -_{s} A) \cdot_{s} (B -_{s} w))\})$

Metamath Proof Explorer

Theorem mulsunif2

Proof