Theorem mulsproplem4

Description: Lemma for surreal multiplication. Under the inductive hypothesis, the product of a member of the old set of A and a member of the old set of B is a surreal number. (Contributed by Scott Fenton, 4-Mar-2025)

	Ref	Expression
Hypotheses	mulsproplem.1	No typesetting found for |- ( ph -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
	mulsproplem4.1	$$⊢\phi \to X\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
	mulsproplem4.2	$$⊢\phi \to Y\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
Assertion	mulsproplem4	Could not format assertion : No typesetting found for |- ( ph -> ( X x.s Y ) e. No ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mulsproplem.1	Could not format ( ph -> A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) ) A. a e. No A. b e. No A. c e. No A. d e. No A. e e. No A. f e. No ( ( ( ( bday ` a ) +no ( bday ` b ) ) u. ( ( ( ( bday ` c ) +no ( bday ` e ) ) u. ( ( bday ` d ) +no ( bday ` f ) ) ) u. ( ( ( bday ` c ) +no ( bday ` f ) ) u. ( ( bday ` d ) +no ( bday ` e ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) -> ( ( a x.s b ) e. No /\ ( ( c ( ( c x.s f ) -s ( c x.s e ) )
2		mulsproplem4.1	$$⊢\phi \to X\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
3		mulsproplem4.2	$$⊢\phi \to Y\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
4		oldssno	$$⊢\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\subseteq \mathrm{No}$$
5	4 2	sselid	$$⊢\phi \to X\in \mathrm{No}$$
6		oldssno	$$⊢\mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)\subseteq \mathrm{No}$$
7	6 3	sselid	$$⊢\phi \to Y\in \mathrm{No}$$
8		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
9	8	a1i	Could not format ( ph -> 0s e. No ) : No typesetting found for |- ( ph -> 0s e. No ) with typecode |-
10		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
11	10 10	oveq12i	Could not format ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) ) : No typesetting found for |- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) ) with typecode |-
12		0elon	$$⊢\varnothing \in \mathrm{On}$$
13		naddrid	Could not format ( (/) e. On -> ( (/) +no (/) ) = (/) ) : No typesetting found for |- ( (/) e. On -> ( (/) +no (/) ) = (/) ) with typecode |-
14	12 13	ax-mp	Could not format ( (/) +no (/) ) = (/) : No typesetting found for |- ( (/) +no (/) ) = (/) with typecode |-
15	11 14	eqtri	Could not format ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/) : No typesetting found for |- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/) with typecode |-
16	15 15	uneq12i	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = ( (/) u. (/) ) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = ( (/) u. (/) ) with typecode |-
17		un0	$$⊢\varnothing \cup \varnothing =\varnothing$$
18	16 17	eqtri	Could not format ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = (/) : No typesetting found for |- ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) = (/) with typecode |-
19	18 18	uneq12i	Could not format ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = ( (/) u. (/) ) : No typesetting found for |- ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = ( (/) u. (/) ) with typecode |-
20	19 17	eqtri	Could not format ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = (/) : No typesetting found for |- ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) = (/) with typecode |-
21	20	uneq2i	Could not format ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. (/) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( ( bday ` X ) +no ( bday ` Y ) ) u. (/) ) with typecode |-
22		un0	Could not format ( ( ( bday ` X ) +no ( bday ` Y ) ) u. (/) ) = ( ( bday ` X ) +no ( bday ` Y ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` Y ) ) u. (/) ) = ( ( bday ` X ) +no ( bday ` Y ) ) with typecode |-
23	21 22	eqtri	Could not format ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` X ) +no ( bday ` Y ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) = ( ( bday ` X ) +no ( bday ` Y ) ) with typecode |-
24		oldbdayim	$$⊢X\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\to \mathrm{bday}\left(X\right)\in \mathrm{bday}\left(A\right)$$
25	2 24	syl	$$⊢\phi \to \mathrm{bday}\left(X\right)\in \mathrm{bday}\left(A\right)$$
26		oldbdayim	$$⊢Y\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)\to \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(B\right)$$
27	3 26	syl	$$⊢\phi \to \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(B\right)$$
28		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
29		bdayelon	$$⊢\mathrm{bday}\left(B\right)\in \mathrm{On}$$
30		naddel12	Could not format ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` X ) e. ( bday ` A ) /\ ( bday ` Y ) e. ( bday ` B ) ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( ( bday ` X ) e. ( bday ` A ) /\ ( bday ` Y ) e. ( bday ` B ) ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
31	28 29 30	mp2an	Could not format ( ( ( bday ` X ) e. ( bday ` A ) /\ ( bday ` Y ) e. ( bday ` B ) ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( ( bday ` X ) e. ( bday ` A ) /\ ( bday ` Y ) e. ( bday ` B ) ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
32	25 27 31	syl2anc	Could not format ( ph -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
33		elun1	Could not format ( ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) with typecode |-
34	32 33	syl	Could not format ( ph -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` X ) +no ( bday ` Y ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) with typecode |-
35	23 34	eqeltrid	Could not format ( ph -> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) u. ( ( ( bday ` 0s ) +no ( bday ` 0s ) ) u. ( ( bday ` 0s ) +no ( bday ` 0s ) ) ) ) ) e. ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( ( ( bday ` C ) +no ( bday ` E ) ) u. ( ( bday ` D ) +no ( bday ` F ) ) ) u. ( ( ( bday ` C ) +no ( bday ` F ) ) u. ( ( bday ` D ) +no ( bday ` E ) ) ) ) ) ) with typecode |-
36	1 5 7 9 9 9 9 35	mulsproplem1	Could not format ( ph -> ( ( X x.s Y ) e. No /\ ( ( 0s ( ( 0s x.s 0s ) -s ( 0s x.s 0s ) ) ( ( X x.s Y ) e. No /\ ( ( 0s ( ( 0s x.s 0s ) -s ( 0s x.s 0s ) )
37	36	simpld	Could not format ( ph -> ( X x.s Y ) e. No ) : No typesetting found for |- ( ph -> ( X x.s Y ) e. No ) with typecode |-