Theorem muls01

Description: Surreal multiplication by zero. (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	muls01	$$⊢A\in \mathrm{No}\to A{\cdot }_s{0}_s=0_s$$

Proof

Step	Hyp	Ref	Expression
1		0no	$$⊢0_s\in \mathrm{No}$$
2		mulsval	$$⊢\left(A\in \mathrm{No}\wedge 0_s\in \mathrm{No}\right)\to A{\cdot }_s{0}_s=\left(\left\{a|\exists p\in L\left(A\right)\exists q\in L\left(0_s\right)a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\right\}\cup \left\{b|\exists r\in R\left(A\right)\exists s\in R\left(0_s\right)b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\right\}\right){|}_s\left(\left\{c|\exists t\in L\left(A\right)\exists u\in R\left(0_s\right)c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\right\}\cup \left\{d|\exists v\in R\left(A\right)\exists w\in L\left(0_s\right)d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\right\}\right)$$
3	1 2	mpan2	$$⊢A\in \mathrm{No}\to A{\cdot }_s{0}_s=\left(\left\{a|\exists p\in L\left(A\right)\exists q\in L\left(0_s\right)a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\right\}\cup \left\{b|\exists r\in R\left(A\right)\exists s\in R\left(0_s\right)b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\right\}\right){|}_s\left(\left\{c|\exists t\in L\left(A\right)\exists u\in R\left(0_s\right)c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\right\}\cup \left\{d|\exists v\in R\left(A\right)\exists w\in L\left(0_s\right)d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\right\}\right)$$
4		rex0	$$⊢\neg \exists q\in \varnothing a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)$$
5		left0s	$$⊢L\left(0_s\right)=\varnothing$$
6	5	rexeqi	$$⊢\exists q\in L\left(0_s\right)a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\leftrightarrow \exists q\in \varnothing a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)$$
7	4 6	mtbir	$$⊢\neg \exists q\in L\left(0_s\right)a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)$$
8	7	a1i	$$⊢p\in L\left(A\right)\to \neg \exists q\in L\left(0_s\right)a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)$$
9	8	nrex	$$⊢\neg \exists p\in L\left(A\right)\exists q\in L\left(0_s\right)a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)$$
10	9	abf	$$⊢\left\{a|\exists p\in L\left(A\right)\exists q\in L\left(0_s\right)a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\right\}=\varnothing$$
11		rex0	$$⊢\neg \exists s\in \varnothing b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)$$
12		right0s	$$⊢R\left(0_s\right)=\varnothing$$
13	12	rexeqi	$$⊢\exists s\in R\left(0_s\right)b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\leftrightarrow \exists s\in \varnothing b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)$$
14	11 13	mtbir	$$⊢\neg \exists s\in R\left(0_s\right)b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)$$
15	14	a1i	$$⊢r\in R\left(A\right)\to \neg \exists s\in R\left(0_s\right)b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)$$
16	15	nrex	$$⊢\neg \exists r\in R\left(A\right)\exists s\in R\left(0_s\right)b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)$$
17	16	abf	$$⊢\left\{b|\exists r\in R\left(A\right)\exists s\in R\left(0_s\right)b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\right\}=\varnothing$$
18	10 17	uneq12i	$$⊢\left\{a|\exists p\in L\left(A\right)\exists q\in L\left(0_s\right)a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\right\}\cup \left\{b|\exists r\in R\left(A\right)\exists s\in R\left(0_s\right)b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\right\}=\varnothing \cup \varnothing$$
19		un0	$$⊢\varnothing \cup \varnothing =\varnothing$$
20	18 19	eqtri	$$⊢\left\{a|\exists p\in L\left(A\right)\exists q\in L\left(0_s\right)a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\right\}\cup \left\{b|\exists r\in R\left(A\right)\exists s\in R\left(0_s\right)b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\right\}=\varnothing$$
21		rex0	$$⊢\neg \exists u\in \varnothing c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)$$
22	12	rexeqi	$$⊢\exists u\in R\left(0_s\right)c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\leftrightarrow \exists u\in \varnothing c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)$$
23	21 22	mtbir	$$⊢\neg \exists u\in R\left(0_s\right)c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)$$
24	23	a1i	$$⊢t\in L\left(A\right)\to \neg \exists u\in R\left(0_s\right)c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)$$
25	24	nrex	$$⊢\neg \exists t\in L\left(A\right)\exists u\in R\left(0_s\right)c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)$$
26	25	abf	$$⊢\left\{c|\exists t\in L\left(A\right)\exists u\in R\left(0_s\right)c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\right\}=\varnothing$$
27		rex0	$$⊢\neg \exists w\in \varnothing d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)$$
28	5	rexeqi	$$⊢\exists w\in L\left(0_s\right)d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\leftrightarrow \exists w\in \varnothing d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)$$
29	27 28	mtbir	$$⊢\neg \exists w\in L\left(0_s\right)d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)$$
30	29	a1i	$$⊢v\in R\left(A\right)\to \neg \exists w\in L\left(0_s\right)d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)$$
31	30	nrex	$$⊢\neg \exists v\in R\left(A\right)\exists w\in L\left(0_s\right)d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)$$
32	31	abf	$$⊢\left\{d|\exists v\in R\left(A\right)\exists w\in L\left(0_s\right)d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\right\}=\varnothing$$
33	26 32	uneq12i	$$⊢\left\{c|\exists t\in L\left(A\right)\exists u\in R\left(0_s\right)c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\right\}\cup \left\{d|\exists v\in R\left(A\right)\exists w\in L\left(0_s\right)d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\right\}=\varnothing \cup \varnothing$$
34	33 19	eqtri	$$⊢\left\{c|\exists t\in L\left(A\right)\exists u\in R\left(0_s\right)c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\right\}\cup \left\{d|\exists v\in R\left(A\right)\exists w\in L\left(0_s\right)d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\right\}=\varnothing$$
35	20 34	oveq12i	$$⊢\left(\left\{a|\exists p\in L\left(A\right)\exists q\in L\left(0_s\right)a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\right\}\cup \left\{b|\exists r\in R\left(A\right)\exists s\in R\left(0_s\right)b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\right\}\right){|}_s\left(\left\{c|\exists t\in L\left(A\right)\exists u\in R\left(0_s\right)c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\right\}\cup \left\{d|\exists v\in R\left(A\right)\exists w\in L\left(0_s\right)d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\right\}\right)=\varnothing {|}_s\varnothing$$
36		df-0s	$$⊢0_s=\varnothing {|}_s\varnothing$$
37	35 36	eqtr4i	$$⊢\left(\left\{a|\exists p\in L\left(A\right)\exists q\in L\left(0_s\right)a=\left(\left(p{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}q\right)\right){-}_s\left(p{\cdot }_{s}q\right)\right\}\cup \left\{b|\exists r\in R\left(A\right)\exists s\in R\left(0_s\right)b=\left(\left(r{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}s\right)\right){-}_s\left(r{\cdot }_{s}s\right)\right\}\right){|}_s\left(\left\{c|\exists t\in L\left(A\right)\exists u\in R\left(0_s\right)c=\left(\left(t{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}u\right)\right){-}_s\left(t{\cdot }_{s}u\right)\right\}\cup \left\{d|\exists v\in R\left(A\right)\exists w\in L\left(0_s\right)d=\left(\left(v{\cdot }_s{0}_s\right){+}_s\left(A{\cdot }_{s}w\right)\right){-}_s\left(v{\cdot }_{s}w\right)\right\}\right)=0_s$$
38	3 37	eqtrdi	$$⊢A\in \mathrm{No}\to A{\cdot }_s{0}_s=0_s$$