Theorem mulsproplem3

Description: Lemma for surreal multiplication. Under the inductive hypothesis, the product of A itself 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 ) )
	mulsproplem3.1	$$⊢\phi \to A\in \mathrm{No}$$
	mulsproplem3.2	$$⊢\phi \to Y\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
Assertion	mulsproplem3	Could not format assertion : No typesetting found for |- ( ph -> ( A 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		mulsproplem3.1	$$⊢\phi \to A\in \mathrm{No}$$
3		mulsproplem3.2	$$⊢\phi \to Y\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
4		oldssno	$$⊢\mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)\subseteq \mathrm{No}$$
5	4 3	sselid	$$⊢\phi \to Y\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 ` A ) +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 ` A ) +no ( bday ` Y ) ) u. (/) ) : No typesetting found for |- ( ( ( bday ` A ) +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 ` A ) +no ( bday ` Y ) ) u. (/) ) with typecode |-
20		un0	Could not format ( ( ( bday ` A ) +no ( bday ` Y ) ) u. (/) ) = ( ( bday ` A ) +no ( bday ` Y ) ) : No typesetting found for |- ( ( ( bday ` A ) +no ( bday ` Y ) ) u. (/) ) = ( ( bday ` A ) +no ( bday ` Y ) ) with typecode |-
21	19 20	eqtri	Could not format ( ( ( bday ` A ) +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 ` A ) +no ( bday ` Y ) ) : No typesetting found for |- ( ( ( bday ` A ) +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 ` A ) +no ( bday ` Y ) ) with typecode |-
22		oldbdayim	$$⊢Y\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)\to \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(B\right)$$
23	3 22	syl	$$⊢\phi \to \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(B\right)$$
24		bdayelon	$$⊢\mathrm{bday}\left(Y\right)\in \mathrm{On}$$
25		bdayelon	$$⊢\mathrm{bday}\left(B\right)\in \mathrm{On}$$
26		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
27		naddel2	Could not format ( ( ( bday ` Y ) e. On /\ ( bday ` B ) e. On /\ ( bday ` A ) e. On ) -> ( ( bday ` Y ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` Y ) e. On /\ ( bday ` B ) e. On /\ ( bday ` A ) e. On ) -> ( ( bday ` Y ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
28	24 25 26 27	mp3an	Could not format ( ( bday ` Y ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( bday ` Y ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
29	23 28	sylib	Could not format ( ph -> ( ( bday ` A ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( ( bday ` A ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
30		elun1	Could not format ( ( ( bday ` A ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( bday ` A ) +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 ` A ) +no ( bday ` Y ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) -> ( ( bday ` A ) +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 |-
31	29 30	syl	Could not format ( ph -> ( ( bday ` A ) +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 ` A ) +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 |-
32	21 31	eqeltrid	Could not format ( ph -> ( ( ( bday ` A ) +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 ` A ) +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 |-
33	1 2 5 7 7 7 7 32	mulsproplem1	Could not format ( ph -> ( ( A x.s Y ) e. No /\ ( ( 0s ( ( 0s x.s 0s ) -s ( 0s x.s 0s ) ) ( ( A x.s Y ) e. No /\ ( ( 0s ( ( 0s x.s 0s ) -s ( 0s x.s 0s ) )
34	33	simpld	Could not format ( ph -> ( A x.s Y ) e. No ) : No typesetting found for |- ( ph -> ( A x.s Y ) e. No ) with typecode |-