Theorem mulsproplem2

Description: Lemma for surreal multiplication. Under the inductive hypothesis, the product of a member of the old set of A and B itself 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 ) )
	mulsproplem2.1	$$⊢\phi \to X\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
	mulsproplem2.2	$$⊢\phi \to B\in \mathrm{No}$$
Assertion	mulsproplem2	Could not format assertion : No typesetting found for |- ( ph -> ( X x.s B ) 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		mulsproplem2.1	$$⊢\phi \to X\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
3		mulsproplem2.2	$$⊢\phi \to B\in \mathrm{No}$$
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		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
7	6	a1i	Could not format ( ph -> 0s e. No ) : No typesetting found for |- ( ph -> 0s e. No ) with typecode |-
8		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
9	8 8	oveq12i	Could not format ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) ) : No typesetting found for |- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = ( (/) +no (/) ) with typecode |-
10		0elon	$$⊢\varnothing \in \mathrm{On}$$
11		naddrid	Could not format ( (/) e. On -> ( (/) +no (/) ) = (/) ) : No typesetting found for |- ( (/) e. On -> ( (/) +no (/) ) = (/) ) with typecode |-
12	10 11	ax-mp	Could not format ( (/) +no (/) ) = (/) : No typesetting found for |- ( (/) +no (/) ) = (/) with typecode |-
13	9 12	eqtri	Could not format ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/) : No typesetting found for |- ( ( bday ` 0s ) +no ( bday ` 0s ) ) = (/) with typecode |-
14	13 13	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 |-
15		un0	$$⊢\varnothing \cup \varnothing =\varnothing$$
16	14 15	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 |-
17	16 16	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 |-
18	17 15	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 |-
19	18	uneq2i	Could not format ( ( ( bday ` X ) +no ( bday ` B ) ) 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 ` B ) ) u. (/) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` B ) ) 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 ` B ) ) u. (/) ) with typecode |-
20		un0	Could not format ( ( ( bday ` X ) +no ( bday ` B ) ) u. (/) ) = ( ( bday ` X ) +no ( bday ` B ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` B ) ) u. (/) ) = ( ( bday ` X ) +no ( bday ` B ) ) with typecode |-
21	19 20	eqtri	Could not format ( ( ( bday ` X ) +no ( bday ` B ) ) 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 ` B ) ) : No typesetting found for |- ( ( ( bday ` X ) +no ( bday ` B ) ) 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 ` B ) ) with typecode |-
22		oldbdayim	$$⊢X\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\to \mathrm{bday}\left(X\right)\in \mathrm{bday}\left(A\right)$$
23	2 22	syl	$$⊢\phi \to \mathrm{bday}\left(X\right)\in \mathrm{bday}\left(A\right)$$
24		bdayelon	$$⊢\mathrm{bday}\left(X\right)\in \mathrm{On}$$
25		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
26		bdayelon	$$⊢\mathrm{bday}\left(B\right)\in \mathrm{On}$$
27		naddel1	Could not format ( ( ( bday ` X ) e. On /\ ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` X ) e. ( bday ` A ) <-> ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` X ) e. On /\ ( bday ` A ) e. On /\ ( bday ` B ) e. On ) -> ( ( bday ` X ) e. ( bday ` A ) <-> ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
28	24 25 26 27	mp3an	Could not format ( ( bday ` X ) e. ( bday ` A ) <-> ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( bday ` X ) e. ( bday ` A ) <-> ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
29	23 28	sylib	Could not format ( ph -> ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
30		elun1	Could not format ( ( ( bday ` X ) +no ( bday ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( bday ` X ) +no ( bday ` B ) ) 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 ` B ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( bday ` X ) +no ( bday ` B ) ) 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 |-
31	29 30	syl	Could not format ( ph -> ( ( bday ` X ) +no ( bday ` B ) ) 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 ` B ) ) 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 |-
32	21 31	eqeltrid	Could not format ( ph -> ( ( ( bday ` X ) +no ( bday ` B ) ) 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 ` B ) ) 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 |-
33	1 5 3 7 7 7 7 32	mulsproplem1	Could not format ( ph -> ( ( X x.s B ) e. No /\ ( ( 0s ( ( 0s x.s 0s ) -s ( 0s x.s 0s ) ) ( ( X x.s B ) e. No /\ ( ( 0s ( ( 0s x.s 0s ) -s ( 0s x.s 0s ) )
34	33	simpld	Could not format ( ph -> ( X x.s B ) e. No ) : No typesetting found for |- ( ph -> ( X x.s B ) e. No ) with typecode |-